| The proof language for type conversions |
Internal representation of proofs
Internally, a Proof
instance is encoded by an expression tree of type GEN (which equals Generic), each subtree being either of
type Literal or Compound. The private
conversion routines between the types Proof
and GEN are postfix .v and proof.
The public routines for the syntactic manipulation of proofs are
proof$literal: Literal ->
Proof
literal?: Proof ->
Boolean
convert: Proof ->
Literal
Creation of a leaf, testing whether a proof is a leaf and converting
a leaf to a literal.
postfix (): (Proof, Tuple Proof) ->
Proof
compound?: Proof ->
Boolean
prefix #: Proof ->
Int
postfix []: (Proof, Int) ->
Proof
Creation of a compound tree, testing whether an proof is a compound
tree, obtaining the arity of a compound tree and accessing a child
of a compound tree.
Internal representation of problems
Syntactic utility routines
postfix .components: Proof ->
Proofs
postfix .args: Proof ->
Proofs
postfix .initial: Proof ->
Proofs
postfix .last: Proof ->
Proof
Commodity accessors for the determination of all components of a
compound tree (postfix
.components), of all arguments of a primitive or
function call (postfix
.args), of all but its last arguments (postfix .initial), and its last
argument (postfix
.args).
subst (pr: Proof, what: Proof, by:
Proof): Proof
subst (pr: Proof, t: TABLE):
Proof
Syntactic substitution of what
by by in pr, or of each variable var in the table t by var[t].
General proof logic
$rule (ax: Proof, val: Proof):
Proof
Construct for basic axioms: the axiom ax
corresponds to a type convertability assertion, such as $converts (F, T), and the value val to the algorithm
which implements the conversion. Rules are usually templated using
the $forall construct
Mark a part of a proof as being not yet solved.
$forall (ql: PRGS, pr: Proof):
Proof
$exists (ql: PRGS, pr: Proof):
Proof
Universal and existential quantification.
$implies (p1: Proof, p2: Proof):
Proof
$and (p1: Proof, p2: Proof):
Proof
$or (p1: Proof, p2: Proof):
Proof
Basic logical connectors.
Type conversion logic
converts (t1: TYP, t2: TYP):
Proof
The assertion that the type t1
can be converted into the type t2.
© 2010 Joris van der Hoeven
Permission is granted to copy, distribute and/or modify this document
under the terms of the
GNU General Public License. If you
don't have this file, write to the Free Software Foundation, Inc., 59
Temple Place - Suite 330, Boston, MA 02111-1307, USA.