Rapid explanation of CHalf
By Peter Hancock (home page http://www.dcs.ed.ac.uk/pgh/)
Table of Contents
- Syntax and concepts
- Sugar
This is an extremely quick explanation of Chalf,
a proof editor I have used based on constructive type theory.
As examples, there are scripts for it
here
here
here
here
here
Note that CHalf is obsolete. It is nevertheless
interesting in many ways, and has a very good
implementation by Dan Synek. He wrote it 1995 and justifiably
doesn't want to support it. It is based on ideas and a prototype of Thierry
Coquand. A new type-checker proof assistant called
Agda
has been developed Chalmers.
The semantics is in some ways very intensional, in a manner
reminiscent of Martin-Löf type theory from the 70's: it involves the
notion of a closure. (I don't attempt an explanation of the semantics
here.)
CHalf is written in C and emacs lisp and is fast and small. The editing
interface is a standard emacs mode, which is a front end for a
line mode interpreter. It is a simple and elegant tool for carefully
working out definitions and constructive proofs.
Thomas Hallgren in Chalmers has written an experimental GUI called
alfa, which
provides an alternative, sexier environment for proof editing.
Syntax and concepts
In Chalf one has:
- Functions
-
- functional form:
- ( x : A )-> B
- abstraction form:
- \ x -> b
- application form:
- b a
- Named products
-
- product form:
- sig { x1 : A1, .. }
- tuple form:
- struct { x1=a1, .. }
- selection form:
- a.xi
These let you deal with chunking-up blocks
of formal material, and refer to chunk components by name. Note:
the blocks can be empty, as in sig{},struct{}.
- Named sums
-
- sum form:
- data { $x1 ( y1 : A1, .. , yk : Ak ), .. }
- constructor form:
- $x1 a1 .. ak
- case form:
- case a of { $x1 y1 .. yk -> a1, .. }
Facilities for tagging data with named
constructors. Note: there can be zero tags data{}; and a given
tag may have no data data{..,$xi,..}. The behaviour of constructors
with respect to type-checking is extremely subtle. They exhibit a
kind of polymorphism; they are not functions.
- Lets
- let { x1 = a1 : A1, .. } in a
Lets can be recursive: this is combined with `overwriting' in
a syntax which appears to be broken. However one has access to
arbitrary fixed-point definitions. CHalf has features
that deal with simultaneous definitions, but they appear to
be broken. There is a way to kluge round the bug.
- Sets, Types, Kind, Theories
- Set : Type : Kind, Theory : Kind
- Set, Type, and Kind
are (predicatively) closed under the above constructions.
Theories are collections of definitions of the form theory { x1 =
a1 : A1, .. } , and the definitions within them may be selected
by name as with tuples. Theories are quite difficult to use. One needs
some sugar for introducing their components under new names, such as
is provided by Agda.
Sugar
There is a certain amount of extra sugar that goes with these.
Here is some (I may have forgotten something).
- repeated abstraction form:
- \ x1 .. xk -> a is sugar for
\ x1 -> .. \ xk -> a .
- repeated functional form:
- ( x1 : A1, .. ) -> a is sugar for
( x1 : A1 ) -> .. -> a .
- left hand side parameters:
-
f ( x1 : A1, .. ) = a : A is sugar for
f = \ x1 .. -> a : ( x1 : A1, .. )-> A
- use of `useless variables'
-
In ( x : A )-> B, the variable x may not occur in B, so that
one grumbles about having to think of a name. But it is used by the
proof editor as a default, when one sends the checker an Intro
command.
Comments in half are like this {- .. -}. I am not sure
if they are allowed to be nested.
There is a certain amount of string and sello-tape (which works) which
involves lines looking like C pre-processor include lines. This has to
do with loading a selection of files in the right order into the type-checker.
Unfinished bits are represented like this: [].
Sometime I might try to describe what it is the type-checker does.