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

1. A NAME_S cannot be used as a Type before it has been declared as a unary predicate symbol.

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 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 Tand 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

1. The argument of dom must be a Concept.

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

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