FO[PF]

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 the cross-product of their argument types, T1 ⨯ ... ⨯ Tn.

It introduces “unary predicates in type signature” and partial Interpretations.

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

1. A NAME_S cannot be used as a Type before it has been declared as a unary predicate symbol. This prevents loops in the subtype-of relation.

2. A NAME_S cannot be used as a Type in a ConstructorDeclaration.

3. (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).

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 \(T_1^I ⨯ ... ⨯ T_n^I\).

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 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 Tand any Ti can be a unary predicate) denotes a total function from the set \(T_1^I ⨯ ... ⨯ T_n^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
}

Interpretations

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

Syntax

(no change)

Well-formedness condition

1. (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.

2. 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 : 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 married persons.