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, the domain and codomain of functions, and partial Interpretations.

Subtypes

This section describes how subtypes are declared.

Lexicon

Token

Pattern

Example

SUBSET

<:|⊆

Syntax

FO[PF] adds this production rule:

  Declaration ← 'type' NAME_T [':=' TypeInterpretation] SUBSET NAME_T;

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

Both these declarations say that T is a subtype of T1, i.e., that the interpretation of T is a subset of the interpretation of T1.

Example

vocabulary {
   type LivingBeing := { Bob, Alice, Tom, Garfield, Kermit }
   type Person := { Bob, Alice, Tom} <: LivingBeing
}

Domain and codomain

Lexicon

Token

Pattern

Example

PARTIAL

total|partial

Syntax

FO[PF] adds these production rules:

    SymbolDecl ← NAME_S { ',' NAME_S } ':' [PARTIAL] Signature [Domains];
      Domains ← '(' domain [ ',' 'codomain' ':' name_ST] ')';
      Domains ← '(' 'codomain' ':' name_ST ')';
        domain <- 'domain' ':' name_ST  { TIMES name_ST }

Well-formedness condition

  1. The syntax above can only be used to declare function symbols (not predicate symbols).

  2. A declaration where the PARTIAL token is total cannot have a Domains.

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

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

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

  1. (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 : total T1 * .. * Tn -> T
   f : T1 * .. * Tn -> T (domain: p1*..*pn, codomain: q)
   f : T1 * .. * Tn -> T (domain: p, codomain: q)
   f : partial T1 * .. * Tn -> T

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 first declaration says that f is a total function over T1 * .. * Tn. The total keyword is optional but recommended in that case.

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