# FO[PF]¶

FO[PF] extends FO[Sugar] to allow the use of partial functions,
i.e., n-ary functions that are not totally defined
over the cross-product of their argument types, `T1 ⨯ ... ⨯ Tn`

.

It introduces syntax to declare subtypes,
a subset relation between predicates,
the domain and codomain of functions, and partial `Interpretation`

s.

## Subtypes and subsets¶

This section describes how subtypes and subsets are declared.

**Lexicon**

Token |
Pattern |
Example |
---|---|---|

SUBSET |
`<< |
⊆` |

**Syntax**

FO[PF] adds these production rules:

```
Declaration ← 'type' NAME_T [':=' TypeInterpretation] SUBSET NAME_T;
Declaration ← SymbolDecl '(' NAME_S SUBSET name_ST { TIMES name_ST } ')';
name_ST <- type;
name_ST <- NAME_S;
```

**Well-formedness condition**

(acyclicity) A

`NAME_T`

cannot be used after`SUBSET`

before it has been declared as a type symbol. This prevents loops in the subtype-of relation.(repetition) The

`NAME_S`

before`SUBSET`

must be the name of the declared symbol.(arity) A

`NAME_ST`

occuring in a cross-product must be either a`type`

or a unary predicate. The number of factor in the cross-product must be the arity of the declared symbol.(interpretation) A

`NAME_T`

must be given an interpretation in a vocabulary, theory or structure block.

**Semantics**

Consider these declaration

```
type T << T1
type T := {..} << T1
p : T1 * .. * Tn -> Bool
p : T1 * .. * Tn -> Bool (p << q)
p : T1 * .. * Tn -> Bool (p << q1 * .. * qn)
```

The first two declarations say that `T`

is a subtype of `T1`

, i.e., that the interpretation of `T`

is a subset of the interpretation of `T1`

.

The next 3 declarations say that `p`

has arity `n`

and takes arguments of type `T1 * .. * Tn`

.
The fourth declaration says that `p`

is a subset of `q`

(where `q`

also has type signature `T1 * .. * Tn -> Bool`

).
The fifth declaration says that `p`

is a subset of the cross-product `q1 * .. * qn`

, where the `qi`

are previously-declared unary predicates.

Thanks to the acyclicity of the subtype-of relation, 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 its superset.

**Example**

```
vocabulary {
type LivingBeing := { Bob, Alice, Tom, Garfield, Kermit }
type Person := { Bob, Alice, Tom} << LivingBeing
married : LivingBeing → Bool (married << Person)
}
```

## Domain and codomain¶

**Syntax**

FO[PF] adds these production rules:

```
Declaration ← SymbolDecl '(' 'total' ')';
Declaration ← SymbolDecl '(' domain [ ',' 'codomain' ':' name_ST] ')';
Declaration ← SymbolDecl '(' 'codomain' ':' name_ST ')';
domain <- 'partial'
domain <- 'domain' ':' name_ST { TIMES name_ST }
```

**Well-formedness condition**

(acyclicity) A

`name_ST`

can occur in a domain or codomain only if it has been previously declared.(arity) when the domain is a symbol

`q`

,`q`

must have the same type signature as the declared symbol. When the domain is the cross-product of unary symbols`qi`

, the number of`qi`

must be the arity of the declared symbol, and each`qi`

must have the type`Ti`

of the declared symbol. The arity of the codomain must be one.(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 (aka asymmetric) interpretation of the logic connectives in FO[Core] (including`if.. then..else`

).

(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`

.

**Semantics**

Consider these declarations:

```
f : T1 * .. * Tn -> T (total)
f : T1 * .. * Tn -> T (domain: p1*..*pn, codomain: q)
f : T1 * .. * Tn -> T (domain: p, codomain: q)
f : T1 * .. * Tn -> T (partial)
```

where `T1,..,Tn`

are previously declared (sub)types and `p, p1,.., pn, q`

are previously-declared types or predicates.

All declarations say that `f`

takes arguments of type `T1 * .. * Tn`

.
The `(total)`

keyword is optional but recommended.

The first declaration says that

`f`

is a total function over`T1 * .. * Tn`

.The second declaration says that

`f`

is defined over exactly the cross-products of the sets p1*..*pn, and that its image is a subset of`q`

(`T -> Bool`

).The third declaration says that

`f`

is defined over exactly`p`

(with type signature`T1*..*Tn -> Bool`

), and that its image is a subset of`q`

(`T -> Bool`

).The fourth declaration says that

`f`

is defined over exactly`dom_f`

, where`dom_f`

is an implicitly declared predicate with type signature`T1*..*Tn -> Bool`

.

**Example**

```
vocabulary {
type LivingBeing := { Bob, Alice, Tom, Garfield, Kermit }
type Person := { Bob, ALice, Tom} << LivingBeing
married : LivingBeing → Bool (married << Person)
spouse: LivingBeing → LivingBeing (domain: married, codomain: married)
}
```

## Interpretations¶

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

**Syntax**

(no change)

**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.

**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 : LivingBeing → Bool (married << Person)
spouse: LivingBeing → LivingBeing (domain: married, codomain: married)
}
theory {
person := { Alice, Bob, Tom }
spouse := { Alice → Bob; Bob → Alice }
}
```

This theory implies that `Alice`

and `Bob`

are the only `married`

persons.