 [ -rw-r--r-- 1 peter other 14732 Oct
13 11:59 /home/peter/half/Heyting.half
                   ]

November 9, 1997

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

Contents

1 Introduction 1 2 Definitions 2 3 nilary 3 4 unary 4 5 binary 5 6 quantifier 7 7 Expressions 11

1 Introduction

We look into how to represent formal systems. These notes are some initial ruminations, at the level of ‘pre-syntax’: i.e. the context free abstract syntax.

To give a formal system, we must define in a concrete fashion what are the expressions, formulas and proofs.

The word ‘concrete’ is meant to suggest that given some expression, we can tell whether or not it is a formula, and tell whether or not two things are instances of the same formula. It is not very different from the basic requirement on alphabets: we need to know whether an inscription is an alphabet character, and whether two inscriptions are of the same character.

For conceptual economy it helps to start with a single ‘ambient’ class of expressions. Here we tell some story like Martin-Lof’s story about ‘concrete objects’ in his thesis. They are vehicles for meaning: things that can be communicated using some suitable medium.

(They may contain parts that are not directly commmunicable. We communicate expressions by sending atoms that correspond to constructor form. (Our partner says: ”what form is it?”, then we ”let me see, .. cons!”, then the other ”now consider its tail, what form is it?”. Being able to communicate an expression this we is being able to discharge one’s obligation to explore the structure of the expression to any desired degree.)

For myself, I think one can always take expressions to be graphs. Graphs allow sharing, and also cycles. This means we have things like the one-node cyclic graph that are definitely ‘pseudo’ expressions, or ‘pre-terms’.

(The last paragraph means it is delicate how we communicate bound variable expressions. Imagine our partner wants to discover the actual buffer. So he tells us he has the thing that is to be substituted for the bound variable, and to refer back to him when we gets there. In actual fact, he’s just pretending. So we imagine a network of people all holding fragments of formal material each with their own preferred representation. They collaborate with each other tell decide questions of equality between expressions. )

Expressions can be higher order. But this just means they are expressions with respect to an extended class of expressions. Begin to think about this in the last section.

2 Definitions

El = \ s -> s : ( s : Set )-> Type
,
Heyting

( set : Set {-The set of formal propositions/sets -}

, el : Pow set {-The set of formal proofs/elements of a prop/set -}

  )
= theory
  {

pred {-formal predicates -}

= {-the function assigning to a set the Set of set valued -}

{-functions on its elements -}

\ s -> ( i : el s )-> set
: Pow set
,

EQ {-Leibnitz equality on a formal set -}

= \s a a'->
( p : pred s )->
( j : el (p a) )->
el (p a')
: ( s : set )->
( a : el s, a' : el s )->
Set
,

3 nilary

Theory defining zero-place constants

nilary

= {–}

theory
{
Zero ( c : set )

= {-c is the empty set -}

let
{
  Constructors
      = sig {}
      : Set
,
  Prog ( intro : Constructors )
      = \ P -> sig {}
      : Pow (pred c)
,
  Solve ( intro : Constructors
        , P : pred c
        , Pp : Prog intro P
        )

= {-defining equations for f -}

         \ f -> sig {}
      :  Pow ( ( z : el c )-> el (P z))
}
in
sig
{ intro : Constructors
, elim  : ( P : pred c, Pp : Prog intro P )->

          sig
          { f : ( z : el c )-> el (P z)
          , deq : Solve intro P Pp f
          }
}
: Set

{-end of Zero -}

} {-end of nilary -}

: Theory
,

4 unary

Theory defining one-place logical constants. So far I have only defined Maybe.

unary
( a : set )

= {-attributes of a single formal set -}

theory
{
Maybe ( c : set )

= {-c is the adjunction of a fresh element to a -}

let
{
  Constructors
      = sig
        { fail : el c
        , unit : ( pr : el a )-> el c
        }
      : Set
,
  Prog ( intro : Constructors )
      = \ P ->
         sig
         { fail_p :
               el (P (intro.fail))
         , unit_p :
               ( pr : el a )->
               el (P (intro.unit pr))
         }
      : Pow (pred c)
,
  Solve ( intro : Constructors
        , P : pred c
        , Pp : Prog intro P

        )

= {-defining equations for f -}

         \ f ->
         sig
         {
           fail_e :
               EQ (P (intro.fail))
                  (f (intro.fail))
                  (Pp.fail_p)
         ,
           unit_e :
               ( pr : el a )->
               EQ (P (intro.unit pr))
                  (f (intro.unit pr))
                  (Pp.unit_p pr)
         }
      :  Pow ( ( z : el c )-> el (P z))
}
in
sig
{ intro : Constructors
, elim  : ( P : pred c, Pp : Prog intro P )->
          sig
          { f : ( z : el c )-> el (P z)
          , deq : Solve intro P Pp f
          }
}
: Set

{-end of Maybe -}

, {-Unary -}

END

= {–}

[]
: []

} {-Unary -}

: Theory
,

5 binary

Theory defining two-place logical constants. So far I have only defined Disjunction.

binary
( a : set, b : set )

= {–}

theory
{
Disjunction ( c : set )

= {-c is the disjunction of a and b -}

let
{
Constructors
= sig
{ inl : ( pr : el a )-> el c
, inr : ( pr : el b )-> el c
}
: Set
,
Prog ( intro : Constructors )
= \ P ->
sig
{ inl_h :
      ( pr : el a )->
      el (P (intro.inl pr))
, inr_h :
      ( pr : el b )->
      el (P (intro.inr pr))
}
: Pow (pred c)
,
Solve ( intro : Constructors
, P : pred c
, Pp : Prog intro P
)

= {-defining equations for f -}

\ f ->
sig
{
  inl_e :
      ( pr : el a )->
      EQ (P (intro.inl pr))
         (f (intro.inl pr))
         (Pp.inl_h pr)
,
  inr_e :
      ( pr : el b )->
      EQ (P (intro.inr pr))
         (f (intro.inr pr))
         (Pp.inr_h pr)
}

      :  Pow ( ( z : el c )-> el (P z))
}
in
sig
{ intro : Constructors
, elim  : ( P : pred c )->
          ( Pp : Prog intro P )->
          sig
          {
            f : ( z : el c )-> el (P z)
          ,
            deq : Solve intro P Pp f
          }
}
: Set

{-end of Disjunction -}

,
END

= {–}

[]
: []

} {-Binary -}

: Theory
,

6 quantifier

Theory defining second order logical constants. So far I have only defined Sum

and Product.
quantifier
( dom : set, fam : pred dom )
= {-defines Sum, Product -}
theory
{
Sum ( c : set )

= {-c is the sum of fam over dom -}

let
{
  Constructors
      = sig
        { pair : ( p : el dom
                 , q : el (fam p) ) -> el c
        }
      : Set

,
  Prog ( intro : Constructors )
      = \ P ->
         sig
         { pair_h :
               ( p : el dom, q : el (fam p) )->
               el (P (intro.pair p q))
         }
      : Pow (pred c)
,
  Solve ( intro : Constructors
        , P : pred c
        , Pp : Prog intro P
        )

= {-defining equation for f -}

         \ f ->
         sig
         {
           pair_e :
               ( p : el dom, q : el (fam p) )->
               EQ (P (intro.pair p q))
                 (Pp.pair_h p q)
                 (f (intro.pair p q))
         }
      :  Pow ( ( z : el c )-> el (P z))
}
in
sig
{ intro : Constructors
, elim  : ( P : pred c, Pp : Prog intro P )->
          sig
          { f : ( z : el c )-> el (P z)
          , deq : Solve intro P Pp f
          }
}
: Set

{-end of Sum -}

,
Product ( c : set )

= {-c is the product of fam over dom -}

let
{
  Constructors
      = sig
        { lambda : ( body : (p : el dom)-> el (fam p) )->

                   el c
        }
      : Set
,
  Prog ( intro : Constructors )
      = \ P ->
         sig
         { lambda_p :
               ( body : (p : el dom)-> el (fam p) )->
               el (P (intro.lambda body))
         }
      : Pow (pred c)
,
  Solve ( intro : Constructors
        , P : pred c
        , Pp : Prog intro P
        )

= {-defining equation for f -}

         \ f ->
         sig
         {
           lambda_e :
               ( body : (p : el dom)-> el (fam p) )->
               EQ (P (intro.lambda body))
                 (Pp.lambda_p body)
                 (f (intro.lambda body))
         }
      :  Pow ( ( z : el c )-> el (P z))
}
in
sig
{ intro : Constructors
, elim  : ( P : pred c )->
          ( Pp : Prog intro P )->
          sig
          {
            f : ( z : el c )-> el (P z)
          ,
            deq : Solve intro P Pp f
          }
}
: Set

{-end of Product -}

, {-Quantifier dom fam -}

END

= {–}

     []
   : []

} {-Quantifier dom fam -}

: Theory

, {-Heyting -}

propositional

= {–}

sig
{ or : binop set
, or_rules : ( a : set, b : set )->
             (binary a b).Disjunction (or a b)
, and : binop set
, and_rules : ( a : set, b : set )->
              (quantifier a (\i->b)).Sum (and a b)
, imp : binop set
, imp_rules : ( a : set, b : set )->
              (quantifier a (\i->b)).Product (imp a b)
, false : set
, quodlibet : nilary.Zero false
, true : set
, banal : (unary false).Maybe true
}
: Set

, {-Heyting -}

END

= {–}

[]
: Set

} {-Heyting -}

: Theory

To ‘work within a logic’, one works within a context such as: set : Set,

el :  Pow set, logic :  (Heyting set el).propositional.

7 Expressions

,
Exp
= theory {

{-Datatype of expressions, first effort -}

E ( X : Set )

= {-Expressions where X is the set of variables -}

  data {
    $Var ( x : X )
  ,
    $App ( fun : E X, arg : E X )
  ,
    $Abs ( body : E (maybe X) )

, {-introduces ‘sharing’ -}

{-Maybe need this in block form, hence lists? -}

    $Let ( def : E X, defbody : E (maybe X) )

, {-Because it allows cycles. -}

    $Fix ( def : E (maybe X) )
  }
: Set

, {-vanilla lists -}

List ( X : Set )
= data { $nil, $cons( hd : X, tl : List X)
: Set
,
lookup ( X : Set, rho : List X,

. {-Values -}

Val ( G : Set )
= []
: Set

, {-Substitution -}

Sub ( X : Set, e : E (maybe X), e' : E X )
= case e of
  {
    $Var x ->
         case x of
         { $fail  -> e'
         , $unit a -> $Var a
         }

,
  $App f a -> $App (Sub X f e') (Sub X a e')
,
  $Abs body -> $Let e' e
,
  $Let def defbody -> $Let e' e {-could make a block -}
,
  $Fix def -> $Let e' e
}
: E X
}
: Theory