Principle head normal forms (principle_hnf)

[binghe]

Hi,

This PR adds the definition and some basic properties and lemmas about principle head normal forms (priciple_hnf). A term may have several hnf's, e.g. if any of its hnf can still do beta reductions, then after such reductions the resulting term is still an hnf by definition. The (unique) terminating term of head reduction path is called "principle" hnf: (Definition 8.3.20 [1, p.177])

[principle_hnf_def] (solvableTheory)
⊢ principle_hnf = last ∘ head_reduction_path

Given that the above definition immediately follows solvable terms in the book, all developments are in solvableTheory of the lambda examples.

Obviously, principle_hnf M is specified only if has_hnf M or solvable M, because otherwise head_reduction_path M is infinite and there's no last element at all. Below are some basic properties of principle hnf:

• The principle hnf of a term is itself if the term is already a hnf:

[principle_hnf_eq_self]
⊢ ∀M. hnf M ⇒ principle_hnf M = M

• (As a consequence of the previous one) Repeated call of principle_hnf reduces to just one:

[principle_hnf_stable]
⊢ ∀M. has_hnf M ⇒ principle_hnf (principle_hnf M) = principle_hnf M

• If M one-step head reduces to N, then M and N have the same principle hnf (NOTE: this sounds like principle hnf is the normal form of head reductions but I'm not sure if the normal_form in chap3Theory can be used)

principle_hnf_hreduce1
⊢ ∀M N. M -h-> N ⇒ principle_hnf M = principle_hnf N

• principle_hnf can be used to do one-step beta reduction if the inner term is already a hnf:

principle_hnf_beta
⊢ ∀v t. hnf t ∧ y # t ⇒ principle_hnf (LAM v t @@ VAR y) = [VAR y/v] t

The last theorem is a generalization of the above one, showing that principle_hnf can be used to eliminate the outer abstractions of hnf in explicit form, when applied to a list of fresh variables, and the result is a nice tpm of inner term:

[principle_hnf_LAMl_appstar]
⊢ ∀t xs ys.
    hnf t ∧ ALL_DISTINCT xs ∧ ALL_DISTINCT ys ∧ LENGTH xs = LENGTH ys ∧
    DISJOINT (set xs) (set ys) ∧ DISJOINT (set ys) (FV t) ⇒
    principle_hnf (LAMl xs t ·· MAP VAR ys) = tpm (ZIP (xs,ys)) t

Regards,

Chun TIAN

[1] Barendregt, H.P.: The Lambda Calculus, Its Syntax and Semantics.
College Publications, London (1984).

[binghe]

NOTE: at the end of solvableScript.sml, I've put a small piece of commented code, trying to prove unsolvable Omega but failed:

(* FIXME: how to leverage Omega_starloops and prove this theorem?
Theorem unsolvable_Omega :
    unsolvable Omega
Proof
   ‘closed Omega’ by rw [closed_def]
 >> rw [solvable_alt_closed]
 >> CCONTR_TAC
 >> ‘?Z. Omega @* Ns -b->* Z /\ I -b->* Z’ by METIS_TAC [lameq_CR]
 >> fs [bnf_reduction_to_self]
 >> Q.PAT_X_ASSUM ‘closed Omega’ K_TAC
 >> POP_ASSUM K_TAC (* Z = I *)
 >> cheat
QED
 *)

Need help ...

[binghe]

Added a more general version of hnf_cases:

hnf_cases_genX
⊢ ∀X. FINITE X ⇒
      ∀M. hnf M ⇔
          ∃vs args y.
            ALL_DISTINCT vs ∧ (M = LAMl vs (VAR y ·· args)) ∧
            DISJOINT (set vs) X

[binghe]

NOTE: at the end of solvableScript.sml, I've put a small piece of commented code, trying to prove unsolvable Omega but failed:

(* FIXME: how to leverage Omega_starloops and prove this theorem?
Theorem unsolvable_Omega :
    unsolvable Omega
Proof
   ‘closed Omega’ by rw [closed_def]
 >> rw [solvable_alt_closed]
 >> CCONTR_TAC
 >> ‘?Z. Omega @* Ns -b->* Z /\ I -b->* Z’ by METIS_TAC [lameq_CR]
 >> fs [bnf_reduction_to_self]
 >> Q.PAT_X_ASSUM ‘closed Omega’ K_TAC
 >> POP_ASSUM K_TAC (* Z = I *)
 >> cheat
QED
 *)

Need help ...

I've done this by myself.