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 aType
before it has been declared as a unary predicate symbol.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 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 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. These conditions also apply to theInterpretation
ofdom(`σ)
.
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
.