{-
\begin{verbatim} Time-stamp: "1997-10-13 11:59:16 peter" #include "./standard.half" #include "./Boole.half" \end{verbatim}
\tableofcontents
\section{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.
-}
{-
\section{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 \texttt{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
,
{-
\section{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 \texttt{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
,
{-
\section{unary}
Theory defining one-place logical constants. So far I have only defined \texttt{Maybe}.
-}
unary
( a : set )
= {- attributes of a single formal set -}
theory
{
Maybe ( c : set )
= {- c is the adjunction of a fresh element to \texttt{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 \texttt{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
,
{-
\section{binary}
Theory defining two-place logical constants. So far I have only defined \texttt{Disjunction}.
-}
binary
( a : set, b : set )
= {- -}
theory
{
Disjunction ( c : set )
= {- c is the disjunction of \texttt{a} and \texttt{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 \texttt{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
,
{-
\section{quantifier}
Theory defining second order logical constants. So far I have only defined \texttt{Sum} and \texttt{Product}.
-}
quantifier
( dom : set, fam : pred dom )
= {- defines \texttt{Sum}, \texttt{Product} -}
theory
{
Sum ( c : set )
= {- c is the sum of \texttt{fam} over \texttt{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 \texttt{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 \texttt{fam} over \texttt{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 \texttt{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: \texttt{set : Set}, \texttt{el : Pow set}, \texttt{logic : (Heyting set el).propositional}.
-}
{-
\section{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