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

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

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

2. (repetition) The NAME_S before SUBSET must be the name of the declared symbol.

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

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

1. (acyclicity) A name_ST can occur in a domain or codomain only if it has been previously declared.

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

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

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

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