Consider:

Inductive [nat:Prop] Constructors [Z:nat][S:nat->nat]; [one = S Z][two = S one][three = S two][four = S three][five = S four]; [add [n,m:nat] = nat_iter ([_:nat]nat) m ([_,x:nat]S x) n];

We add a new non-canonical constant:

[NCC:nat->nat] [||NCC (S(S(S Z))) ==> Z];

(Remark about a minor modification to LEGO rewrite syntax).

In old versions, `Hnf NCC two` would compute to `NCC
two`. This is reasonable, as `NCC two` *is* a whnf
(or canonical form): no amount of computation can change its outermost
constructor. Similarly, `Hnf NCC (add one one)` would produce
`NCC (add one one)`. However, although `NCC two` and
`NCC (add one one)` are canonical forms, in order to discover
this, LEGO had to compute the arguments `two` and `add one
one` to `S(S Z)`, and ascertain that this doesn't match
with `S(S(S Z))`, so you might think `Hnf NCC (add one
one)` should produce `NCC (S(S Z))`, by analogy with beta
and projection. For example `Hnf (([x:nat->nat]x) f Z)`, where
`f` is a variable, produces `f Z` by updating the head
of the application, even though the outermost constructor,
application, is not changed by this updating. Similarly `Hnf
(([x:nat#nat]x) f).1` produces `f.1`. The difference is
that beta and projection update the head (root) of an expression, even
if they don't change the outer constructor, but rewriting would update
the arguments, and not even just "top-level" arguments.

Nonetheless, the original decision not to do pattern updating in LEGO, now seems to have been a poor choice, and the new version does pattern updating.

BTW, notice that in the example above we also have `Hnf NCC
five` returns `NCC (S(S(S(S one))))`, because LEGO unwinds
the argument just far enough to see that it is not `three`.

Pattern updating brings LEGO's computation very much in line with that of a lazy functional language such as Haskell, except that LEGO's patterns may be non-linear.

Last modified: 13-Feb-1997