Rapid explanation of CHalf

By Peter Hancock (home page http://www.dcs.ed.ac.uk/pgh/)

Table of Contents

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.