+December 2011, Chris Pressey, Cat's Eye Technologies
+Madison is a language in which one can state proofs of properties
+of term-rewriting systems. Classical methods of automated reasoning,
+such as resolution, are not used; indeed, term-rewriting itself is
+used to check the proofs. Both direct proof and proof by induction
+are supported. Induction in a proof must be across a structure which
+has a well-founded inductive definition. Such structures can be
+thought of as types, although this is largely nominal; the traditional
+typelessness of term-rewiting systems is largely retained.
+Madison has at its core a simple term-rewriting language. It is of
+a common form which should be unsurprising to anyone who has worked
+at all with term rewriting. A typical simple program contains
+a set of rules and a term on which to apply those rules. Each
+rule is a pair of terms; either term of the pair may contain
+variables, but any variable that appears on the r.h.s must also
+appear on the l.h.s. A rule matches a term if is the same as
+the term with the exception of the variables, which are bound
+to its subterms; applying a matching rule replaces the term
+with the r.h.s. of the rule, with the variables expanded approp-
+riately. Rules are applied in an innermost, leftmost fashion to
+the term, corresponding to eager evaluation. Rewriting terminates
+when there is no rule whose l.h.s. matches the current incarnation
+of the term being rewritten.
+A term is either an atom, which is a symbol that stands alone,
+or a constructor, which is a symbol followed by a comma-separated list
+of subterms enclosed in parentheses. Symbols may consist of letters,
+digits, and hyphens, with no intervening whitespace. A symbol is
+a variable symbol if it begins with a capital letter. Variable
+symbols may also begin with underscores, but these may only occur
+in the l.h.s. of a rewrite rule, to indicate that we don't care
+what value is bound to the variable and we won't be using it on
+(The way we are using the term "constructor" may be slightly non-
+standard; in some other sources, this is called a "function symbol",
+and a "constructor" is a subtly different thing.)
+Because the rewriting language is merely a component (albeit the
+core component) of a larger system, the aforementioned typical
+simple program must be cast into some buttressing syntax. A full
+program consists of a `let` block which contains the rules
+and a `rewrite` admonition which specifies the term to be re-
+written. An example follows.
+| leftmost(tree(X,Y)) -> leftmost(X)
+| leftmost(leaf(X)) -> X
+| rewrite leftmost(tree(tree(leaf(alice),leaf(grace)),leaf(dan)))
+In the above example, there are two rules for the constructor
+`leftmost/1`. The first is applied to the outer tree to obtain
+a new leftmost constructor containing the inner tree; the first
+is applied again to obtain a new leftmost constructor containing
+the leaf containing `alice`; and the second is applied to that
+leaf term to obtain just `alice`. At that point, no more rules
+apply, so rewriting terminates, yielding `alice`.
+Madison is deterministic; if rules overlap, the first one given
+(syntactically) is used. For this reason, it is a good idea
+to order rules from most specific to least specific.
+I used the phrase "typical simple program" above because I was
+trying intentionally to avoid saying "simplest program". In fact,
+technically no `let` block is required, so you can write some
+really trivial Madison programs, like the following:
+I think that just about covers the core term-rewriting language.
+Term-rewriting is Turing-complete, so Madison is too. If you
+wish to learn more about term rewriting, there are several good
+books and webpages on the subject; I won't go into it further
+My desire with Madison was to design a language in which you
+can prove things. Not a full-blown theorem prover -- just a
+proof checker, where you supply a proof and it confirms either
+that the proof holds or doesn't hold. (Every theorem prover
+has at its core a proof checker, but it comes bundled with a lot of
+extra machinery to search the space of possible proofs cleverly,
+looking for one which will pass the proof-checking phase.)
+It's no coincidence that Madison is built on top of a term-rewriting
+language. For starters, a proof is very similar to the execution
+trace of a term being rewritten. In each of the steps of the proof,
+the statement to be proved is transformed by replacing some part
+of it with some equally true thing -- in other words, rewritten.
+In fact, Post Canonical Systems were an early kind of rewriting
+system, devised by Emil Post to (as I understand it) illustrate this
+similarity, and to show that proofs could be mechanically carried out
+So: given a term-rewriting language, we can give a trivial kind
+of proof simply by stating the rewrite steps that *should* occur
+when a term is rewritten, and check that proof by rewriting the term
+and confirming that those were in fact the steps that occurred.
+For the purpose of stating these sequences of rewrite steps to be
+checked, Madison has a `theorem..proof..qed` form. To demonstrate
+this form, let's use Madison to prove that 2 + 2 = 4, using Peano
+| add(s(X),Y) -> add(X,s(Y))
+| add(s(s(z)),s(s(z))) ~> s(s(s(s(z))))
+| -> add(s(z),s(s(s(z)))) [by add.1]
+| -> add(z,s(s(s(s(z))))) [by add.1]
+| -> s(s(s(s(z)))) [by add.2]
+The basic syntax should be fairly apparent. The `theorem` block
+contains the statement to be proved. The `~>` means "rewrites
+in zero or more steps to". So, here, we are saying that 2 + 2
+(in Peano notation) rewrites, in zero or more steps, to 4.
+The `proof` block contains the actual series of rewrite steps that
+should be carried out. For elucidation, each step may name the
+particular rule which is applied to arrive at the transformed term
+at that step. Rules are named by their outermost constructor,
+followed by a dot and the ordinal position of the rule in the list
+of rules. These rule-references are optional, but the fact that
+the rule so named was actually used to rewrite the term at that step
+could be checked too, of course. The `qed` keyword ends the proof
+Naturally, you can also write a proof which does not hold, and
+Madison should inform you of this fact. 2 + 3, for example,
+does not equal 4, and it can pinpoint exactly where you went
+wrong should you come to this conclusion:
+| add(s(X),Y) -> add(X,s(Y))
+| add(s(s(z)),s(s(s(z)))) ~> s(s(s(s(z))))
+| add(s(s(z)),s(s(s(z))))
+| -> add(s(z),s(s(s(s(z))))) [by add.1]
+| -> add(z,s(s(s(s(z))))) [by add.1]
+| -> s(s(s(s(z)))) [by add.2]
+? Error in proof [line 6]: step 2 does not follow from applying [add.1] to previous step
+Now, while these *are* proofs, they don't tell us much about the
+properties of the terms and rules involved, because they are not
+*generalized*. They say something about a few fixed values, like
+2 and 4, but they do not say anything about any *infinite*
+sets of values, like the natural numbers. Now, that would be *really*
+useful. And, while I could say that what you've seen of Madison so far
+is a proof checker, it is not a very impressive one. So let's take
+To state a generalized proof, we will need to introduce variables,
+and to have variables, we will need to be able to say what those
+variables can range over; in short, we need *quantification*. Since
+we're particularly interested in making statements about infinite
+sets of values (like the natural numbers), we specifically want
+*universal quantification*:
+But to have universal quantification, we first need a *universe*
+over which to quantify. When we say "for all /x/", we generally
+don't mean "any and all things of any kind which we could
+possibly name /x/". Rather, we think of /x/ as having a type of
+ For all natural numbers x, ...
+Then, if our proof holds, it holds for all natural numbers.
+No matter what integer value greater than or equal to zero
+we choose for /x/, the truism contained in the proof remains true.
+This is the sort of thing we want in Madison.
+Well, to start, there is one glaringly obvious type in any
+term-rewriting language, namely, the term. We could say
+But it would not actually be very interesting, because terms
+are so general and basic that there's not actually very much you
+can say about them that you don't already know. You sort of need
+to know the basic properties of terms just to build a term-rewriting
+language (like the one at Madison's core) in the first place.
+The most useful property of terms as far as Madison is concerned is
+that the subterm relationship is _well-founded_. In other words,
+in the term `c(X)`, `X` is "smaller than" `c(X)`, and since terms are
+finite, any series of rewrites which always results in "smaller" terms
+will eventually terminate. For completeness, we should probably prove
+that rigorously, but for expediency we will simply take it as a given
+Anyway, to get at something actually interesting, we must look further
+than the terms themselves.
+What's actually interesting is when you define a restricted
+set of forms that terms can take, and you distinguish terms inside
+this set of forms from the terms outside the set. For example,
+| boolean(false) -> true
+| rewrite boolean(false)
+We call a set of forms like this a _type_. As you can see, we
+have basically written a predicate that defines our type. If any
+of the rewrite rules in the definition of this predicate rewrite
+a given term to `true`, that term is of our type; if it rewrites
+Once we have types, any constructor may be said to have a type.
+By this we mean that no matter what subterms the constructor has,
+the predicate of the type of which we speak will always reduce to
+`true` when that term is inserted in it.
+Note that using predicates like this allows our types to be
+non-disjoint; the same term may reduce to true in two different
+predicates. My first sketches for Madison had disjoint types,
+described by rules which reduced each term to an atom which named
+the type of that term. (So the above would have been written with
+rules `true -> boolean` and `false -> boolean` instead.) However,
+while that method may be, on the surface, more elegant, I believe
+this approach better reflects how types are actually used in
+programming. At the end of the day, every type is just a predicate,
+and there is nothing stopping 2 from being both a natural number and
+an integer. And, for that matter, a rational number and a real
+In theory, every predicate is a type, too, but that's where things
+get interesting. Is 2 not also an even number, and a prime number?
+And in an appropriate (albeit contrived) language, is it not a
+description of a computation which may or may not always halt?
+The above considerations motivate us to be careful when dealing
+with types. We should establish some ground rules so that we
+know that our types are useful to universally quantify over.
+Unfortunately, this introduces something of a chicken-and-egg
+situation, as our ground rules will be using logical connectives,
+while at the same time they will be applied to those logical
+connectives to ensure that they are sound. This is not, actually,
+a big deal; I mention it here more because it is interesting.
+So, the rules which define our type must conform to certain
+rules, themselves. While it would be possible to allow the
+Madison programmer to use any old bunch of rewrite rules as a
+type, and to check that these rules make for a "good" type when
+such a usage is seen -- and while this would be somewhat
+attractive from the standpoint of proving properties of term-
+rewriting systems using term-rewriting systems -- it's not strictly
+necessary to use a descriptive approach such as this, and there are
+certain organizational benefits we can achieve by taking a more
+Viz., we introduce a special syntax for defining a type with a
+set of rules which function collectively as a type predicate.
+Again, it's not strictly necessary to do this, but it does
+help organize our code and perhaps our thoughts, and perhaps make
+an implementation easier to build. It's nice to be able to say,
+yes, what it means to be a `boolean` is defined right here and
+So, to define a type, we write our type rules in a `type..in`
+block, like the following.
+| boolean(false) -> true
+| rewrite boolean(false)
+As you can see, the wildcard reduction to false can be omitted for
+brevity. (In other words, "Nothing else is a boolean" is implied.)
+And, the `boolean` constructor can be used for rewriting in a term
+just like any other plain, non-`type`-blessed rewrite rule.
+| boolean(false) -> true
+| rewrite boolean(tree(leaf(sabrina),leaf(joe)))
+Here are the rules that the type-defining rules must conform to.
+If any of these rules are violated in the `type` block, the Madison
+implementation must complain, and not proceed to try to prove anything
+Once a type is defined, it cannot be defined further in a regular,
+non-type-defining rewriting rule.
+| boolean(false) -> true
+? Constructor "boolean" used in rule but already defined as a type
+The constructor in the l.h.s. must be the same in all rules.
+? In type "foo", constructor "bar" used on l.h.s. of rule
+The constructor used in the rules must be arity 1 (i.e. have exactly
+? In type "foo", constructor has arity greater than one
+It is considered an error if the predicate rules ever rewrite, inside
+the `type` block, to anything besides the atoms `true` or `false`.
+? In type "foo", rule reduces to "bar" instead of true or false
+The r.h.s.'s of the rules of the type predicate must *always*
+rewrite to `true` or `false`. That means, if we can't prove that
+the rules always rewrite to something, we can't use them as type
+predicate rules. In practice, there are a few properties that
+we insist that they have.
+They may involve type predicates that have previously been
+| boolean(false) -> true
+| boolbox(box(X)) -> boolean(X)
+| rewrite boolbox(box(true))
+They may involve certain, pre-defined rewriting rules which can
+be thought of as operators on values of boolean type (which, honestly,
+is probably built-in to the language.) For now there is only one
+such pre-defined rewriting rule: `and(X,Y)`, where `X` and `Y` are
+booleans, and which rewrites to a boolean, using the standard truth
+table rules for boolean conjunction.
+| boolean(false) -> true
+| boolpair(pair(X,Y)) -> and(boolean(X),boolean(Y))
+| rewrite boolpair(pair(true,false))
+| boolean(false) -> true
+| boolpair(pair(X,Y)) -> and(boolean(X),boolean(Y))
+| rewrite boolpair(pair(true,cheese))
+Lastly, the r.h.s. of a type predicate rule can refer to the self-same
+type being defined, but *only* under certain conditions. Namely,
+the rewriting must "shrink" the term being rewritten. This is what
+lets us inductively define types.
+| nat(s(X)) -> nat(s(X))
+? Type not well-founded: recursive rewrite does not decrease in [foo.2]
+| nat(s(X)) -> nat(s(s(X)))
+? Type not well-founded: recursive rewrite does not decrease in [foo.2]
+| bad(tree(X,Y)) -> and(bad(X),bad(tree(Y,Y))
+? Type not well-founded: recursive rewrite does not decrease in [bad.2]
+We can check this by looking at all the rewrite rules in the
+definition of the type that are recursive, i.e. that contain on
+on their r.h.s. the constructor being defined as a type predicate.
+For every such occurrence on the r.h.s. of a recursive rewrite,
+the contents of the constructor must be "smaller" than the contents
+of the constructor on the l.h.s. What it means to be smaller
+should be fairly obvious: it just has fewer subterms. If all the
+rules conform to this pattern, rewriting will eventually terminate,
+because it will run out of subterms to rewrite.
+Application of Types in Proofs
+------------------------------
+Now, aside from these restrictions, type predicates are basically
+rewrite rules, just like any other. The main difference is that
+we know they are well-defined enough to be used to scope the
+universal quantification in a proof.
+Simply having a definition for a `boolean` type allows us to construct
+a simple proof with variables. Universal quantification over the
+universe of booleans isn't exactly impressive; we don't cover an infinite
+range of values, like we would with integers, or lists. But it's
+a starting point on which we can build. We will give some rewrite rules
+for a constructor `not`, and prove that this constructor always reduces
+to a boolean when given a boolean.
+| boolean(false) -> true
+| forall X where boolean(X)
+| boolean(not(X)) ~> true
+| -> boolean(true) [by not.1]
+| -> true [by boolean.1]
+| -> boolean(false) [by not.2]
+| -> true [by boolean.2]
+As you can see, proofs using universally quantified variables
+need to make use of _cases_. We know this proof is sound, because
+it shows the rewrite steps for all the possible values of the
+variable -- and we know they are all the possible values, from the
+In this instance, the cases are just the two possible values
+of the boolean type, but if the type was defined inductively,
+they would need to cover the base and inductive cases. In both
+matters, each case in a complete proof maps to exactly one of
+the possible rewrite rules for the type predicate. (and vice versa)
+Let's prove the type of a slightly more complex rewrite rule,
+one which has multiple subterms which can vary. (This `and`
+constructor has already been introduced, and we've claimed we
+can use it in the definition of well-founded inductive types;
+but this code proves that it is indeed well-founded, and it
+doesn't rely on it already being defined.)
+| and(true,true) -> true
+| forall X where boolean(X)
+| forall Y where boolean(Y)
+| boolean(and(X,Y)) ~> true
+| boolean(and(true,true))
+| -> boolean(true) [by and.1]
+| -> true [by boolean.1]
+| boolean(and(true,false))
+| -> boolean(false) [by and.2]
+| -> true [by boolean.2]
+| boolean(and(false,true))
+| -> boolean(false) [by and.2]
+| -> true [by boolean.2]
+| boolean(and(false,false))
+| -> boolean(false) [by and.2]
+| -> true [by boolean.2]
+Unwieldy, you say! And you are correct. But making something
+easy to use was never my goal.
+Note that the definition of `and()` is a bit more open-ended than
+`not()`. `and.2` allows terms like `and(dog,cat)` to rewrite to `false`.
+But our proof only shows that the result of reducing `and(A,B)` is
+a boolean *when both A and B are booleans*. So it, in fact,
+tells us nothing about the type of `and(dog,cat)`, nor in fact anything
+at all about the properties of `and(A,B)` when one or more of `A` and
+`B` are not of boolean type. So be it.
+Anyway, since we were speaking of inductively defined types
+previously, let's do that now. With the help of `and()`, here is
+a type for binary trees.
+| tree(branch(X,Y)) -> and(tree(X),tree(Y))
+| rewrite tree(branch(leaf,leaf))
+We can define some rewrite rules on trees. To start small,
+let's define a simple predicate on trees.
+| tree(branch(X,Y)) -> and(tree(X),tree(Y))
+| empty(branch(_,_)) -> false
+| in empty(branch(branch(leaf,leaf),leaf))
+| tree(branch(X,Y)) -> and(tree(X),tree(Y))
+| empty(branch(_,_)) -> false
+Now let's prove that our predicate always rewrites to a boolean
+(i.e. that it has boolean type) when its argument is a tree.
+| tree(branch(X,Y)) -> and(tree(X),tree(Y))
+| empty(branch(_,_)) -> false
+| forall X where tree(X)
+| boolean(empty(X)) ~> true
+| -> boolean(true) [by empty.1]
+| -> true [by boolean.1]
+| boolean(empty(branch(S,T)))
+| -> boolean(false) [by empty.2]
+| -> true [by boolean.2]
+This isn't really a proof by induction yet, but it's getting closer.
+This is still really us examining the cases to determine the type.
+But, we have an extra guarantee here; in `case X = branch(S,T)`, we
+know `tree(S) -> true`, and `tree(T) -> true`, because `tree(X) -> true`.
+This is one more reason why `and(X,Y)` is built-in to Madison; it
+needs to leverage what it means and make use of this information in a
+proof. We don't really use that extra information in this proof, but
+Let's try something stronger, and get into something that could be
+described as real structural induction. This time, we won't just prove
+something's type. We'll prove something that actually walks and talks
+like a real (albeit simple) theorem: the reflection of the reflection
+of any binary tree is the same as the original tree.
+| tree(branch(X,Y)) -> and(tree(X),tree(Y))
+| reflect(branch(A,B)) -> branch(reflect(B),reflect(A))
+| forall X where tree(X)
+| reflect(reflect(X)) ~> X
+| reflect(reflect(leaf))
+| -> reflect(leaf) [by reflect.1]
+| -> leaf [by reflect.1]
+| reflect(reflect(branch(S, T)))
+| -> reflect(branch(reflect(T),reflect(S))) [by reflect.2]
+| -> branch(reflect(reflect(S)),reflect(reflect(T))) [by reflect.2]
+| -> branch(S,reflect(reflect(T))) [by IH]
+| -> branch(S,T) [by IH]
+Finally, this is a proof using induction! In the [by IH] clauses,
+IH stands for "inductive hypothesis", the hypothesis that we may
+assume in making the proof; namely, that the property holds for
+"smaller" instances of the type of X -- in this case, the "smaller"
+trees S and T that are used to construct the tree `branch(S, T)`.
+Relying on the IH is valid only after we have proved the base case.
+After having proved `reflect(reflect(S)) -> S` for the base cases of
+the type of S, we are free to assume that `reflect(reflect(S)) -> S`
+in the induction cases. And we do so, to rewrite the last two steps.
+Like cases, the induction in a proof maps directly to the
+induction in the definition of the type of the variable being
+universally quantified upon. If the induction in the type is well-
+founded, so too will be the induction in the proof. (Indeed, the
+relationship between induction and cases is implicit in the
+concepts of the "base case" and "inductive case (or step)".)
+So, we have given a simple term-rewriting-based language for proofs,
+and shown that it can handle a proof of a property over an infinite
+universe of things (trees.) That was basically my goal in designing
+this language. Now let's step back and consider some of the
+implications of this system.
+We have, here, a typed programming language. We can define types
+that look an awful lot like algebraic data types. But instead of
+glibly declaring the type of any given term, like we would in most
+functional languages, we actually have to *prove* that our terms
+always rewrite to a value of that type. That's more work, of
+course, but it's also stronger: in proving that the term always
+rewrites to a value of the type, we have, naturally, proved that
+it *always* rewrites -- that its rewrite sequence is terminating.
+There is no possibility that its rewrite sequence will enter an
+infinite loop. Often, we establish this with the help of previously
+established basis that our inductively-defined types are well-founded,
+which is itself proved on the basis that the subterm relationship is
+Much like we can prove termination in course of proving a type,
+we can prove a type in the course of proving a property -- such
+as the type of `reflect(reflect(T))` above. (This does not directly
+lead to a proof of the type of `reflect`, but whatever.)
+And, of course, we are only proving the type of term on the
+assumption that its subterms have specific types. These proofs
+say nothing about the other cases. This may provide flexibility
+for extending rewrite systems -- or it might not, I'm not sure.
+It might be nice to prove that all other types result in some
+error term. (One of the more annoying things about term-rewriting
+languages is how an error can result in a half-rewritten program
+instead of a recgonizable error code. There seems to be a tradeoff
+between extensibility and producing recognizable errors.)
+I think I've described everything I want in the language above, so
+the grammar should, modulo tweaks, look something like this:
+ Block ::= LetBlock | TypeBlock | ProofBlock | RewriteBlock.
+ LetBlock ::= "let" {Rule} "in" Block.
+ TypeBlock ::= "type" Symbol "is" {Rule} "in" Block.
+ RewriteBlock ::= "rewrite" Term.
+ Rule ::= Term "->" Term.
+ Term ::= Atom | Constructor | Variable.
+ Constructor ::= Symbol "(" Term {"," Term} ")".
+ ProofBlock ::= "theorem" Statement "proof" Proof "qed".
+ Statement ::= Quantifier Statement | MultiStep.
+ Quantifiers ::= "forall" Variable "where" Term.
+ MultiStep ::= Term "~>" Term.
+ Proof ::= Case Proof {Case Proof} | Trace.
+ Trace ::= Term {"->" Term [RuleRef]}.
+ RuleRef ::= "[" "by" (Symbol "." Integer | "IH") "]".
+I think that basically covers it. This document is still a little
+rough, but that's what major version zeroes are for, right?
+I have essentially convinced myself that the above-described system
+is sufficient for simple proof checking. There are three significant
+things I had to convince myself of to get to this point, which I'll
+One is that types have to be well-founded in order for them to serve
+as scopes for universal quantification. This is obvious in
+retrospect, but getting them into the language in a way where it was
+clear they could be checked for well-foundedness took a little
+effort. The demarcation of type-predicate rewrite rules was a big
+step, and a little disappointing because it introduces the loaded
+term `type` into Madison's vernacular, which I wanted to avoid.
+But it made it much easier to think about, and to formulate the
+rules for checking that a type is well-founded. As I mentioned, it
+could go away -- Madison could just as easily check that any
+constructor used to scope a universal quantification is well-founded.
+But that would probably muddy the presentation of the idea in this
+document somewhat. It would be something to keep in mind for a
+subsequent version of Madison that further distances itself from the
+Also, it would probably be possible to extend the notion of well-
+founded rewriting rules to mutually-recursive rewriting rules.
+However, this would complicate the procedure for checking that a
+type predicate is well-founded.
+The second thing I had to accept to get to this conviction is that
+`and(X,Y)` is built into the language. It can't just be defined
+in Madison code, because while this would be wonderful from a
+standpoint of minimalism, Madison has to know what it means to let
+you write non-trivial inductive proofs. In a nutshell, it has to
+know that `foo(X) -> and(bar(X),baz(X))` means that if `foo(X)` is
+true, then `bar(X)` is also true, and `baz(X)` is true as well.
+I considered making `or(X,Y)` a built-in as well, but after some
+thought, wasn't convinced that it was that valuable in the kinds
+of proofs I wanted to write.
+Lastly, the third thing I had to come to terms with was, in general,
+how we know a stated proof is complete. As I've tried to describe
+above, we know it's complete because each of the cases maps to a
+possible rewrite rule, and induction maps to the inductive definition
+of a type predicate, which we know is well-founded because of the
+checks Madison does on it (ultimately based on the assumption that
+the subterm property is well-founded.) There Is Nothing Else.
+This gets a little more complicated when you get into proofs by
+induction. The thing there is that we can assume the property
+we want to prove, in one of the cases (the inductive case) of the
+proof, so long as we have already proved all the other cases (the
+base case.) This is perfectly sound in proofs by hand, so it is
+likewise perfectly sound in a formal proof checker like Madison;
+the question is how Madison "knows" that it is sound, i.e. how it
+can be programmed to reject proofs which are not structured this
+way. Well, if we limit it to what I've just described above --
+check that the scope of the universal quantification is well-
+founded, check that there are two cases, and check that we've already
+proved one case, then allow the inductive hypothesis to be used as a
+rewrite rule in the other case of the proof -- this is not difficult
+to see how it could be mechanized.
+However, this is also very limited. Let's talk about limitations.
+For real data structures, you might well have multiple base cases;
+for example, a tree with two kinds of leaf nodes. Does this start
+breaking down? Probably. It probably breaks down with multiple
+inductive cases, as well, although you might be able to get around
+that with breaking the proof into multiple proofs, and having
+subsequent proofs rely on properties proved in previous proofs.
+Another limitation I discovered when trying to write a proof that
+addition in Peano arithmetic is commutative. It seemingly can't
+be done in Madison as it currently stands, as Madison only knows
+how to rewrite something into something else, and cannot express
+the fact that two things (like `add(A,B)` and `add(B,A)`) rewrite
+to the same thing. Such a facility would be easy enough to add,
+and may appear in a future version of Madison, possibly with a
+You would then show that `add(A,B)` reduces to something, and
+that `add(B,A)` reduces to something, and Madison would check
+that the two somethings are in fact the same thing. This is, in
+fact, a fairly standard method in the world of term rewriting.
+As a historical note, Madison is one of the pieces of fallout from
+the overly-ambitious project I started a year and a half ago called
+Rho. Rho was a homoiconic rewriting language with several very
+general capabilities, and it wasn't long before I decided it was
+possible to write proofs in it, as well as the other things it was
+designed for. Of course, this stretched it to about the limit of
+what I could keep track of in a single project, and it was soon
+afterwards abandoned. Other fallout from Rho made it into other
+projects of mine, including Pail (having `let` bindings within
+the names of other `let` bindings), Falderal (the test suite from
+the Rho implementation), and Q-expressions (a variant of
+S-expressions, with better quoting capabilities, still forthcoming.)