3.2. FO in FO(·): Expressions

3.2 FO in FO(·)

In IDP-Z3, we express knowledge in FO(·). This language is an extension of classical first-order logic (FO).

We start by discussing expressions, which are the basic building blocks of formulas.

3.2.1 Expressions

Formulas are built out of expressions. Each expression represents a value of a certain type. Expressions are constructed by applying functions or built-in operators to the other expressions of the correct type. For instance, the expression 5 + 1 - 2 represents the value 4 of the built-in type Int. Because it uses only built-in types and operators, this expression is rigid: its value does not depend on the context in which we consider the expression.

Once our expressions also include symbols that we define ourselves in the vocabulary, they will typically no longer be rigid. For instance, in the vocabulary AgeVoc, we previously wrote down the expression sonsAge() * 2 +1. This expression is non-rigid: to know which value of type Int it represents, we need a structure that tells us what the function sonsAge looks like. However, the vocabulary does already tell us that expression is correctly typed, since sonsAge() is of type Int.

Exercise

Consider the following vocabulary

vocabulary ExVoc { type R type T type S foo: (R * T) -> S bar: (S) -> R g: () -> R h: () -> S i: () -> T }

For each of the following expressions, indicate whether the expression is correct and, if so, what its type is:

Expression	Correct?	Type
`foo(g(), h())`
`bar(h())`
`h(bar())`
`bar(foo(bar(h()), i()))`

Exercise

Consider the following structure for the above vocabulary ExVoc:

structure S: ExVoc { R := {1, 2, 3}. S := {a, b, c}. T := {4, 5}. foo: := {(1,4) -> a, (2,4) -> b, (3,4) -> c, (1,5) -> a, (2,5) -> b, (3,5) -> c}. bar := {a -> 1, b -> 2, c -> 3}. g := 2. h := b. i := 4. }

What is the value of the expression bar(foo(bar(h()), i())) in this structure?

The type of an expression is always completely determined by the vocabulary in which the expression is written. The possible values of this type, on the other hand, may depend on the particular structure in which the expression is considered. For instance, the structure AgeStrucFuncBase we saw earlier defines that the possible values for type Person are Me and MySon, but other structures may assign a different set of possible values to this type, thereby changing the set of possible values that an expression of type Person could have.

So far, we have always declared types in a vocabulary and enumerated their possible values in a structure. It is also possible to enumerate the values of a type immediately in the vocabulary itself: this has the effect of making the type rigid, in the sense that all structures for this vocabulary must now have the same interpretation for this type.

For example, the following are two structures (DotWS1 and DotWS2) for the same vocabulary, each of which assigns a different set of values to the type DayOfTheWeek. This example also illustrates the special notation that is used inside a structure to enumerate predicates (i.e., functions with boolean range): instead of writing each DayOfTheWeek and mapping it to true/false, the enumeration of the predicate weekend simply lists all of the days for which weekend(day) = true; all days that are not mentioned are mapped to the value false.

vocabulary DotWVoc { type DayOfTheWeek weekend: DayOfTheWeek -> Bool } structure DotWS1: DotWVoc { DayOfTheWeek := { Mo, Tu, We, Th, Fr, Sa, Su }. weekend := { Sa, Su }. } structure DotWS2: DotWVoc { DayOfTheWeek := { 1, 2, 3}. weekend := { 1, 2 }. }

By constrast, the following vocabulary fixes a rigid set of values for the type DayOfTheWeek.

vocabulary DotWVoc { type DayOfTheWeek := { Mo, Tu, We, Th, Fr, Sa, Su } weekend: DayOfTheWeek -> Bool } structure DotWS1: DotWVoc { weekend := { Sa, Su }. }

Making the values of the type rigid in this way also allows them to be used in a theory directly, as from the theory's perspective, these values have been declared. For instance, this allows us to move the enumeration of the predicate weekend from a structure to a theory (the "~" symbol represents the boolean operator "not").

vocabulary DotWVoc { type DayOfTheWeek := { Mo, Tu, We, Th, Fr, Sa, Su } weekend: DayOfTheWeek -> Bool } structure DotWS1: DotWVoc { } theory DotWTh: DotWVoc { weekend(Sa). weekend(Su). ~weekend(Ma). ~weekend(Tu). ~weekend(We). ~weekend(Th). ~weekend(Fr). }

In general, if you want to refer to specific non-numerical domain elements in your theory, you'll want to define its values in the vocabulary like in the example above.