##
Aldor examples

##
Simon Thompson

This page has links to programs which implement logic in the
computer algebra system Aldor, as described in this paper, presented at
Calculemus 2000.

###
Project overview

###
Logic: equality types and rules for Boolean

eqType.as

An I-type in Aldor. Uses pretend in two ways:
- to implement the rules for I-types, and
- to ensure that type checking proceeds correctly.
Uses the rules to derive symmetry and transitivity of I-equality.

boolElim.as

Dependently typed elimination rules for Booleans.
Uses pretend to sidestep the type system of Aldor.

###
Axiomatising monoids and groups: Booleans as monoids

monGrpAx.as

Axiomatising monoids and groups using paremetrised categories and
inheritance. Neat. Includes eqType.as for I-types.
monGrpAx2.as

Axiomatising monoids and groups using category extension.

boolMonRaw.as

Booleans as a monoid: no encapsulation, just top level
declarations of the functions involved.

boolMondAx2.as

Booleans as a monoid: the definition is done by defining a new
domain, BoolMonoid, whose representation type is Boolean.
The `raw' definitions of the functions over Boolean are included
from the file boolMonRaw.as.

The category of BoolMondoid is MonoidAndAx, which is an extension
of Monoid with the axioms, rather than a free-standing set of
(proofs of) the axioms. It is defined in
monGrpAx2.as.

boolMondAx3.as

The previous example, refactored.

###
Vectors

vector.as

A type of Integer Vectors; Vector(n), given a recursive type
definition. Also defines constructors, print function, addition and
vector append. Uses pretend heavily to reassure the type checker.
The programs don't just type check but actually work too!

###
Logic

propLogic2.as

Propositional logic in Aldor.
Encapsulation is used here to hide any non type correct stuff
(use of pretend) inside elementary introduction and elimination
rules. Given these one can assemble proofs in a completely
acceptable way using the type system of Aldor.

predLogic1-1.as

Predicate logic in Aldor: in particular Exists.

predLogic2-1.as

Predicate logic in Aldor: universal quantification and a proof
that exists/forall implies forall/exists.

predLogic3-1.as

Predicate logic in Aldor: universal quantification and a proof
that exists/forall implies forall/exists. (Uses an encapsulated
version of the universal type.)

Last modified 21 August 2000.