# FO[PF] ?¶

Note

This extension is work-in-progress.

FO[PF] extends FO[Sugar] to allow the use of partial functions (including partial predicates),
i.e., n-ary functions that are not totally defined over `T1 ⨯ ... ⨯ Tn`

.

It introduces “unary predicates in type signature”, the `partial`

and `dom`

keywords,
and special rules for `Interpretation`

.

## Unary predicates in type signature¶

This section describes how unary predicates can be used to specify the domain and range of partial functions.

**Syntax**

FO[PF] adds this production rule:

```
Type ← NAME_S;
```

**Well-formedness condition**

A

`NAME_S`

cannot be used as a`Type`

before it has been declared as a**unary predicate**symbol.A

`NAME_S`

cannot be used as a`Type`

in a`ConstructorDeclaration`

.(Well-guardedness) Logic formulas in a theory must be

*well-guarded*to ensure that the value of functions outside of their domain has no influence on the truth value of the theory. This can be achieved by using binary quantification and the non-strict interpretation of the logic connectives in FO[Core] (including`if.. then..else`

).

**Semantics**

A unary predicate `P`

with signature `T → Bool`

denotes a subset \(P^I\) of \(T^I\) in structure \(I\).
A unary predicate `Q`

with signature `P → Bool`

denotes a subset \(Q^I\) of \(P^I\).
A n-ary predicate `R`

with signature `T1 ⨯ ... ⨯ Tn → Bool`

(where any `Ti`

can be a unary predicate)
denotes a subset \(R^I\) of \(T1^I ⨯ ... ⨯ Tn^I\).

Thus, a predicate `P`

always denotes a subset of a cross-product of type(s).
This cross-product is determined by (recursively) looking up the signature of `P`

.

A function `f`

with signature `P → Q`

denotes a *total* function from the set \(P^I\) to the set \(Q^I\).
The function has no value outside of \(P^I\).
A function `f`

with signature `T1 ⨯ ... ⨯ Tn → T`

(where `T`

and any `Ti`

can be a unary predicate)
denotes a *total* function from the set \(T1^I ⨯ ... ⨯ Tn^I\) to the set \(T^I\).

(For FO[ID]) A definition of `f`

must define a value in the range of `f`

for all tuples of arguments in the domain of `f`

.

**Example**

```
vocabulary {
type LivingBeing:= { Bob, Alice, Tom, Garfield, Kermit }
person : LivingBeing → Bool
married : person → Bool
spouse: married → married
}
```

`Partial`

and `dom`

keywords¶

This section presents a alternative way to declare partial functions, for use when the domain is not a cross-product of sets.

**Syntax**

```
Declaration ← { ANNOT } 'partial' NAME_S { ',' NAME_S } ':' Signature;
Symbol ← 'dom' '(' Expression ')';
```

**Well-formedness condition**

The argument of

`dom`

must be a Concept.(Well-guardedness) Logic formulas in a theory must be

*well-guarded*to ensure that the value of functions outside of their domain has no influence on the truth value of the theory. This can be achieved by using binary quantification and the non-strict interpretation of the logic connectives in FO[Core] (including`if.. then..else`

).

**Semantics**

For a function `f`

declared as `partial f: T1 ⨯ ... ⨯ Tn → T`

,
formula `dom(`f)`

denotes the subset of `T1 ⨯ ... ⨯ Tn`

that is the domain of `f`

,
i.e., the set of (tuple of) values for which `f`

is defined.
Thus, the signature of `dom(`f)`

is `T1 ⨯ ... ⨯ Tn → Bool`

.
The signature of `f`

may use unary predicates.

(For FO[ID]) A definition of `f`

must define a value of the appropriate type for all tuples of arguments in the domain of `f`

.

**Example**

```
vocabulary {
partial f: Real ⨯ Real → Real
}
theory {
{ !x,y in Real: dom(`f)(x,y) ← x ≠ y.
!x,y in dom(`f): f(x,y) = 1/(x-y). }
}
```

## Interpretations¶

This section discusses the (possibly partial) interpretation of partial functions.

**Syntax**

FO[PF] adds these production rules:

```
Interpretation ← 'dom' '(' '`{NAME_S}' ')' ':=' SymbolInterpretation '.';
```

**Well-formedness condition**

(Partial predicate) Unlike in FO[Core], the

`Interpretation`

of a predicate`p`

may use the`→`

element, followed by`true`

or`false`

. When it uses the`→`

element, it must use it for every`TupleValue`

, and it may also use the`else`

clause.The

`Value`

in the`Interpretation`

of a symbol`σ`

must be in the domain and range of`σ`

. The`Interpretation`

of`σ`

must be total over its domain. These conditions are checked at the syntax level when the`Interpretation`

of the domain and/or range of`σ`

is explicitly and totally given. These conditions also apply to the`Interpretation`

of`dom(`σ)`

.

**Semantics**

If the `Interpretation`

of `σ`

is total and has no `else`

part, it also specifies the interpretation of the domain of `σ`

.

**Example**

```
vocabulary {
type LivingBeing:= { Bob, Alice, Tom, Garfield, Kermit }
person : LivingBeing → Bool
married : person → Bool
spouse: married → married
}
theory {
person := { Alice, Bob, Tom }
spouse := { Alice → Bob; Bob → Alice }
}
```

This theory implies that `Alice`

and `Bob`

are the only `spouse`

.