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

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.)