Go backward to 5 Partial function spaces and partial types
Go up to Top
Go forward to 7 Subsorting

# 6 Predicate types

Design proposal: There is a special sort truth. Predicates are total functions into truth (partial functions into truth are disallowed). These total functions are denoted with a different arrow, because for functions into truth, application is not the standard application. Instead, false is delivered if the function term or the argument term is undefined. This is needed to stay within the two-valued logic.

Examples:
 op and:(t => truth ×t => truth) => truth var x:t; P,Q:t => logical axiom and(P,Q)(x) <=> P(x) /\ Q(x)

In (an encoding of) a temporal logic, we would have a sort time, and truth values are predicates time => logical. Then a predicate everytime:(time => logical) => logical could be defined as everytime(p) <=> forall t:time.p(t)

Another advantage is that user-defined logical connectives become possible:
 op xor:(truth ×truth) => truth var x,y:truth axioms xor(x,y) <=> (¬x <=> y) ...xor(phi,psi) ...

Alternatives:

1. Enrich the current proposal by allowing also pred(t) as a synonym for t => truth in order to be consistent with first-order CASL. (This is more a matter of syntax.)
2. Modify the current proposal by requiring pred(t) instead of t => truth (so functions into truth are disallowed). (Again, this is more a matter of syntax.)
3. Modify the current proposal by dropping the special sort truth and adding a type constructor pred, which gives for any type t the type pred(t) of predicates over t, instead. As before, an application of a predicate term to an argument term yields false, if the predicate term or the argument term is undefined.

With this, we loose the possibility to have user-defined logical connectives in a convenient manner. We have to write:
 op xor:pred(pred() ×pred()) var P,Q:pred() axioms xor(P,Q) <=> (¬P() <=> Q()) ...xor(\x:().phi,\x:().psi) ...

4. There is a type constructor pred, but the set of admissible types is restricted [Far91] in order to guarantee that each predicate term is defined. Call a type predicative, if it is of form pred(t) or if it is a function type whose result type is predicative. For each predicative type, there is a canonical value given by \x1....\xn.false. A type is admissible if it is not forbidden and all its components are admissible. Forbidden types are partial function types with non-predicative codomain.

Then, predicate application is defined as follows: The predicate term is always defined by the above restriction of the type system. If the argument term is undefined, yield the canonical value, otherwise, apply the predicate.

This alternative is a s which still captures all practically needed cases. But since the restriction rather adds complexity instead of reducing complexity, we do not find it so useful.

5. Predicate types are allowed only at the top level. This rules out many useful examples (cf. above).

CoFI Note: L-8 ---- 7 January 1998.