[lambda] Rank-based fresh name allocations; stage work on boehmTheory

[binghe]

Hi,

This PR contains the (finally settled) Rank-based fresh name allocations (implemented in basic_swapTheory) and the (reworked) Böhm theory up to Proposition 10.3.7 (i) [1, p.248] (Boehm out lemma). I think the work is stable enough (after being revisited several times) and statements committed definitions and theorems will unlikely be changed again.

There are a lot of file changes in this PR, and many of them are cleanup & maintenance work. The core changes are in the following two files only:

• examples/lambda/basics/basic_swapScript.sml
• examples/lambda/barendregt/boehmScript.sml

The central idea here is a new way for allocating fresh names for the binding variables in Böhm trees. We know that the set of all strings is countably infinite, and in string_numTheory we have the s2n and n2s functions as bijections between strings and natural numbers. Furthermore, by using npair/nfst/nsnd from numpairTheory, each natural number has a bijection to a pair of natural numbers. Combining these two work, this means that, in theory we can imagine a two-dimension infinite table of strings, the string at row i and column j is n2s (npair i j) (aka n2s (i *, r)). The following primitive function alloc can be used to "allocate" a list of string at row r, with columns ranged from m to n:

[alloc_def] (basic_swapTheory)
⊢ ∀r m n. alloc r m n = MAP (n2s ∘ $*, r) [m ..< n]

(NOTE: [m ..< n] is from listRangeTheory. It is the list of natural numbers ranged from m to n-1.)

Now let's think how to "allocate" n fresh names which is disjoint with a given finite set of string (usually comes from FV t, the free variables of a λ-term.) Given any finite set of strings, the following function string_width can be used to find out the maximal "column" of the strings in it, if we put these string into the above imaginary 2-dimensional table:

[string_width_def]
⊢ ∀s. string_width s = MAX_SET (IMAGE (nsnd ∘ s2n) s)

Let d = SUC string_width s, then we can see that alloc r d (d + n) will give us a list fresh names of size n, and they must be disjoint with the set s, because the "column" of strings in s are all smaller than d, while the newly allocated strings have larger columns. And they are all at the r-th row. Below is the definition of this RNEWS function:

[RNEWS]
⊢ ∀r n s. RNEWS r n s = (let d = SUC (string_width s) in alloc r d (d + n))

Furthermore, ROW r is the infinite set of all string at the row r. And RANK r is the set of all strings at rows < r:

[ROW_DEF]
⊢ ∀r. ROW r = IMAGE (λi. n2s (r ⊗ i)) 𝕌(:num)

[RANK_DEF]
⊢ ∀r. RANK r = BIGUNION (IMAGE ROW (count r))

The ranked fresh names are used in the definition of Böhm trees and the corresponding subterm: The binding variables used at the Böhm tree level r (root level is 0) are from the same row, allocated by RNEWS: (vs = RNEWS r n X)

[BT_generator_def]
⊢ ∀X M r.
    BT_generator X (M,r) =
    if solvable M then
      (let
         M0 = principle_hnf M;
         n = LAMl_size M0;
         vs = RNEWS r n X;
         M1 = principle_hnf (M0 ·· MAP VAR vs);
         Ms = hnf_children M1;
         y = hnf_headvar M1;
         l = MAP (λe. (e,SUC r)) Ms
       in
         (SOME (vs,y),fromList l))
    else (NONE,[||])

[subterm_def]
⊢ (∀X M r. subterm X M [] r = SOME (M,r)) ∧
  ∀X M h p r.
    subterm X M (h::p) r =
    if solvable M then
      (let
         M0 = principle_hnf M;
         n = LAMl_size M0;
         vs = RNEWS r n X;
         M1 = principle_hnf (M0 ·· MAP VAR vs);
         Ms = hnf_children M1;
         m = LENGTH Ms
       in
         if h < m then subterm X (EL h Ms) p (SUC r) else NONE)
    else NONE

This changes makes sure that Böhm trees generated from different terms, as long as they excluded the same X, these trees all use the same binding variables at the same levels, and thus is totally comparable.

As a consequence, most theorems in boehmTheory now have three universally quantified variables !X M r where r is the initial row/rank. And all Böhm theorems having induction-based proofs now have antecedents FV M SUBSET X UNION RANK r instead of the previous FV M SUBSET X. The following "subterm induction lemma" is typical:

[subterm_induction_lemma]
⊢ ∀X M r M0 n m vs M1 Ms h.
    FINITE X ∧ FV M ⊆ X ∪ RANK r ∧ solvable M ∧ M0 = principle_hnf M ∧
    n = LAMl_size M0 ∧ vs = RNEWS r n X ∧
    M1 = principle_hnf (M0 ·· MAP VAR vs) ∧ Ms = hnf_children M1 ∧
    m = LENGTH Ms ∧ h < m ⇒
    FV (EL h Ms) ⊆ X ∪ RANK (SUC r)

The following [Boehm_transform_exists_lemma], the previously extra tpm_rel in the main conclusion is now elimianated (subterm' X (apply pi M) q r = [P/v] (subterm' X M q r)), rendering this lemma better aligned with textbook:

[Boehm_transform_exists_lemma]
⊢ ∀X M p r.
    FINITE X ∧ FV M ⊆ X ∪ RANK r ∧ p ≠ [] ∧ subterm X M p r ≠ NONE ⇒
    ∃pi.
      Boehm_transform pi ∧ is_ready' (apply pi M) ∧
      FV (apply pi M) ⊆ X ∪ RANK (SUC r) ∧
      ∃v P.
        closed P ∧
        ∀q. q ≼ p ∧ q ≠ [] ⇒
            subterm X (apply pi M) q r ≠ NONE ∧
            subterm' X (apply pi M) q r = [P/v] (subterm' X M q r)

Other changes include some new theorems about IS_PREFIX and listRange in core theories, some theorem modern syntax changes, and I added some header comments for theories of the lambda examples.

Chun

[1] Barendregt, H.P.: The lambda calculus, its syntax and semantics. College Publications, London (1984).