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 Interpretation
s.
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 aType
before it has been declared as a unary predicate symbol. This prevents loops in the subtype-of relation.A
NAME_S
cannot be used as aType
in aConstructorDeclaration
.(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 T
and 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
(Partial predicate) Unlike in FO[Core], the
Interpretation
of a predicatep
may use the→
element, followed bytrue
orfalse
. When it uses the→
element, it must use it for everyTupleValue
, and it may also use theelse
clause.The
Value
in theInterpretation
of a symbolσ
must be in the domain and range ofσ
. TheInterpretation
ofσ
must be total over its domain. These conditions are checked at the syntax level when theInterpretation
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.