                           premise.demon.co.uk
 [ -rw-r--r-- 1 peter other 11977 Oct
13 11:59 /home/peter/half/world.half ]

November 9, 1997

Time-stamp:  "1997-10-13 11:59:43 peter"
#include "./standard.half"
#include "./Boole.half"

How to organise the ‘facilities’ for simple structures? Take ‘worlds’ as an example.

Contents

1 Theory of worlds 1 1.1 Debris . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

1 Theory of worlds

A world consists of a set, and a predicate defined on it. Think of the elements of the domain set as propositions (or types), and the predicate as a truth predicate.

By the Curry-Howard correspondence, we can also think of the predicate as a set valued family indexed by the base set. The set corresponding to a proposition is the set of its proofs, and to say that the proposition is true is to say the set has an element.

So we can say that the notion of a world is a constructive formulation of what from the classical point of view would be described as a set (of formal propositions) together with a subset of it (the formally provable propositions). It is a much richer notion constructively, because we have a much richer notion of ‘truth-value’ (of course, one can express this constructively as well, with labour).

The interest of worlds is largely that they can function as formal universes - that is, they can in many situations play the role of the framework’s (large) universe:

Set :  Type
El =  s -> s :  ( s :  Set )-> Type

yet they are small, and mathematically managable:

set :  Set
el =  s -> el s :  ( s :  El set )-> Set .
World
= theory
{

t = the type of a world

   Fam Set
: Type
,
m ( U : Set, T : Pow U )

= how to make a world

  struct { I = U, g = T }
: t
,
example0
= m empty.set (empty.fun Set)
: t
,
example1 ( given : t )

= Von Neumann successor

  m (maybe given.I)
    (\ a ->
     case a of {  $fail  -> given.I
               ,  $unit a1 -> given.g a1
               }
    )
: t
,
f ( us : Fam t )
= let
  { I = us.I : Set
  , g = us.g : ( i : I )-> t
  , U = \i->(g i).I : Pow I
  , T = \i -> (g i).g  : ( i : I)-> Pow (U i)
  }
  in theory
     { sum = m (Sigma I U) (\iu->T iu.p iu.q)

   : t
, prod = m (Pi I U) (\i2u -> Pi I (\i->T i (i2u i)))
    : t
}
: Theory
,
i ( me : t )

= attributes and properties of a single instance

theory

{ standard names for the components

U = me.I : Set
,
T = me.g : Pow U
,
inhabited
= sig { witness : U
    , proof : T witness
    }
: Set
,
inconsistent
= ( a : U  )-> T a
: Set

, World.i me

keeping the set U fixed.

lattice ( T' : Pow U )
= theory
{ ops ( a : U )
     = theory
        { cap = and (T a) (T' a) : Set
        , cup = or (T a) (T' a) : Set
        , subseteq = arrow (T a) (T' a) : Set
        , supseteq = arrow (T' a) (T a) : Set
        }

: Theory (World.i me).lattice.ops a

, LE = ( a : U )-> (ops a).subseteq : Set
, GE = ( a : U )-> (ops a).supseteq : Set
, EQ = sig { le : LE, ge : GE } : Set
, cap = \ a -> (ops a).cap : Pow U
, cup = \ a -> (ops a).cap : Pow U
, exhaustive = ( a : U )-> (ops a).cup : Set
, disjoint   = ( a : U )-> empty.set : Set
, consistent = sig { witness : U
                   , proof : (ops witness).cap
                   } : Set

      , END = [] : []
      }

: Theory (World.i me).lattice

some more sanitary formulations

, LE = \ T' -> (lattice T').LE : Quantifier U
, GE = \ T' -> (lattice T').GE : Quantifier U
, EQ = \ T' -> (lattice T').EQ : Quantifier U
, cap = \ T' -> (lattice T').cap : OP (Pow U)
, cup = \ T' -> (lattice T').cap : OP (Pow U)
, complement = \a->( a : U )-> empty.set : Pow U

, World.i me

  binary ( other : t )

= things to do with 2 worlds

      let { U' = other.I : Set
          , T' = other.g : Pow U'
          }
      in theory

{ To = set of maps from me to other

                sig {  u : fun U U'
                    ,  t : Pi U (\x->fun (T x) (T' (u x)))
                    }
              : Set

, From = set of maps from other to me

                  sig {  u : fun U' U
                      ,  t : Pi U' (\x->fun (T' x) (T (u x)))
                      }
                : Set
         , add = m (or U U') (\a'->case a' of {
                                   $inl a -> T a,
                                   $inr b -> T' b})
               : t
         , mul = m (and U U') (\a->and (T a.p) (T' a.q))
               : t
         }

: Theory (World.i me).binary

, World.i me

some convenient forms: (World x).i.Maps.To y

  Maps =  theory

{ To = returns set of maps to another world

                 \ other -> (binary other).To
               : Pow t

,

From = returns set of maps from another world

         \ other -> (binary other).From
       : Pow t
}

: Theory (World.i me).Maps

,
it = me : t
}

: Theory World.i me

}
: Theory World
,

World' Merging into above ( A : Set, B : Pow A ) components of a world. = Something to be merged in

theory
{ Inhabited = Sigma A B : Set B is a non-empty predicate
, Universal = Pi A B : Set  B holds universally

We can think of A as a small universe of sets, and B as its decoding function. This leads to a number of definitions.

, Relative  = theory
{ set = A : Set
, el  = B : Pow set
, pow = \ X -> ( x : X )-> set : OP Set
, pow' = \ s -> pow (el s) : ( s : set )-> Set
, fam = \ X -> sig { d : set
                   , p : ( i : el d )-> X } : OP Set
, rel = \ X -> ( x : X )-> pow X : OP Set
, ts  = \ X -> ( x : X )-> fam X : OP Set
, quant = \ X -> pow (pow X) : OP Set
, famfam = \ X -> fam (fam X) : OP Set
, pands = \ X -> ( x : X )-> famfam X : OP Set
}
: Theory

the ‘subseteq’ relation

, LE        = \ B' -> ( a : A , hyp : B a )-> B' a
: Pow (Pow A)

, GE        = \ B' -> ( a : A , hyp : B' a )-> B a
: Pow (Pow A)
, EQ        = \ B' -> and (LE B') (GE B')
: Pow (Pow A)

binary operations

, cap       = \ B' a ->and (B a) (B' a)
: OP (Pow A)
, cup       = \ B' a ->or (B a) (B' a)
: OP (Pow A)

operations on families of predicates

, Cap ( B' : Fam (Pow A) )
= \a->Pi B'.I (\i->B'.g i a)
: Pow A
, Cup ( B' : Fam (Pow A) )
= \a->Sigma B'.I (\i->B'.g i a)
: Pow A

a universe containing this world, closed under a quantifier

, QClosure
( Q : (A : Set)-> Quantifier A )
= let
{ Phi ( x : World.t ) the operator we fix
= let { wx = World.i x : Theory,
    U = wx.U : Set, T = wx.T : Pow U }
in
World.m
  ( data

{ $A code for this world

, $B ( a : A ) codes for the sets in this world , $Q codes for sets of quantifier form

         ( domain : U
         , predicate : ( x : T domain )-> U
         )
    } )
  ( \ u ->
    case u of
    { $A  -> A
    , $B a -> B a

, $Q d p -> Q (T d) (\ a -> T (p a))
} )
: World.t
, x = Phi x : World.t
}
in x
: World.t
, QClosureOP( Q : ( A : Set )-> Quantifier A)

= throws in one level of the quantifier

\ AB ->
let { A = (World.i AB).U : Set
, B = (World.i AB).T : Pow A
, A'= data
{ $already_there ( a : A )
, $q ( a : A
     , b : ( x : B a )-> A
     )
}
: Set
, B'= \ u ->
case u of
{ $already_there a -> B a
, $q a b -> Q (B a) (\ x -> B (b x))
}
: Pow A'
}
in
World.m A' B'

: OP (World.t) fixed point of this is closed under Q

}
: Theory

1.1 Debris

This belongs with the world stuff. Already there?

, SuccU Successor of a family

( AB : Fam Set )
= let { A = AB.I : Set
, B = AB.g : ( a : A )-> Set
} in

struct
{ I=data{ $0, $1 ( a : A )}
, g=\i->case i of
 { $0  -> A
 , $1 a1 -> B a1
 }
}
: Fam Set

Least family of sets extending a given family, and closed under an operator from families of sets to families of sets.

belongs with world stuff

, SuperU ( F : ( X : Fam Set )-> Fam Set
, AB : Fam Set )
= let
{ VS = let
{ V  = VS.I : Set
, S  = VS.g : ( v : V )-> Set
, G  ( a : V, b : ( i : S a )-> V)
     = F (struct
          { I=S a
          , g=\i->S (b i)}) : Fam Set
, U  ( a : V, b : ( i : S a )-> V)
     = (G a b).I : Set
, T  ( a : V, b : ( i : S a )-> V)
     = (G a b).g : ( u : U a b )-> Set
} in
    struct
    { I=data
        { $0
        , $1 ( a : AB.I )
        , $u ( a : V
             , b : ( i : S a )-> V )
        , $t ( a : V
             , b : ( i : S a )-> V
             , c : U a b )
        }
    , g=\i->case i of
           { $0  -> AB.I
           , $1 a -> AB.g a
           , $u a b -> U a b
           , $t a b c -> T a b c
           }

}
: Fam Set } in
VS
: Fam Set
,

mark = [] : []