Various Holy Trinities

The greater part of my childhood was spent sitting on church pews: first presbyterian, then high anglican. Various theological images were relentlessly pounded into my brain when it was at its most impressionable. One such image is that of a trinity. Great orators, like St. Paul (faith, hope, charity), Churchill (blood, sweat, tears), Hitler (Ein Volk, ein Reich, ein Feurher -- or was that Goebbles?), and Bill Gates ("One World. One Web. One Program." -- or was that the marketing department?) know well the power of the trinity.

Context, Type, Term. (Peter Dybjer's categories with families.)
       Context : Set, 
       Type    : Context -> Set,
       Term    : (Pi G : Context) Type(G) -> Set, 
       ... then whatever extra structure, eg. 
       ExtType : (Pi G : Context) Ty(G) -> Context, 
       ExtDef  : (Pi G : Context, A : Ty(G)) Tm(G,A) -> Context, 
               -- we allow contexts with definitions. 
There are surely some connections with the next trinity.

Function, relation, predicate transformer. (de Moor, Gardiner, ..)
        Parent, third level:
           Father : A -> Fam(Fam(B))         Mother : A -> Pow(Pow(B))   

        Child, second level:
           Son    : A -> Fam(B)              Daughter : A -> Pow(B)

                                HolyGhost : A -> B
This does not go further because the parent level "lacks pullovers". A pullover is an order enriched isotope of a pullback, something between a cardigan and a pair of flared dungarees. There is a systematic connection between the levels in which the morphisms of a higher level can be modelled as a kind of `span' in the next lower level.
This is maybe a "quintinity".
[ Anton Setzer reports that according to (Jung's interpretation of) Roman Catholic doctrine, sometime around 1963 the Virgin Mary ascended into heaven or achieved godhead. The cardinality of God may now be greater than 3. Or the powerset of natural numbers, or the continuum, for all I know. ]
State-predicate, action, specification. (Lamport)
          pred : Pow(State)
          act  : Pow(State^2)
          spec : Pow(State^w)    -- w is omega = Nat
Lamport says a (closed system) specification has the general form:
                EXISTS aux .  Init /\ []( x # x' => Act)  /\ Liveness
where Liveness is a "countable disjunction" of fairness properties
            WF_x(A) = (<>[]enabled (A /\ x # x')) => []<>(A /\ x # x')
            SF_x(A) = ([]<>enabled (A /\ x # x')) => []<>(A /\ x # x')
and EXISTS aux is a kind of existential quantification over flexible variables that is insensitive to stuttering.

Echo of Julian Bradfield's question of whether modal mu-calculus alternation hierarchy collapses at the third level. (It doesn't!)

Another theological metaphor: To break a safety property is a sin of commission. To break a liveness property is a sin of omission.

Lamports page on TLA , his specification language.

Object, Type, Kind. (de Bruijn)
The reason why this does not go further is probably that rather than introduce another level, we reflect kinds down into types, and then elaborate the new structure in the level of kinds.

An interesting question is to try to characterise as precisely as possible what a "reflection principle" is.

Addition, multiplication, exponentiation.
If we take the usual arithmetic of iterative exponents as definitions of additive combinators (0,+), multiplicative combinators (1,*) and an exponential combinator (^), it is well known that these are combinatorially complete.

Peter Hancock
Last modified: Fri Jun 29 07:23:32 BST 2001