Böhm tree with basic properties

[binghe]

Hi,

This PR finally adds the formalization of Böhm trees (Chapter 10 of [Barendregt 1984]) , an co-inductive tree-like representation of λ terms (based on HOL's ltreeTheory). This work has been revised several times in the past 4 months and the current definition is finally verified by showing two β-equivalent terms have the "same" (to be explained) Böhm tree, thus perhaps it's really correct for the need of later uses. Note also that currently the construction is done without help of de Bruijn encoding, but a further translation (not available yet) of the resulting tree w.r.t. de Bruijn encoding may achieve the uniqueness of Böhm trees for α-equivalent λ-terms.

Let's briefly recall the "textbook construction" of Böhm trees: given an λ-term M, first we need to know if it's solvable. If not, its Böhm tree is a special "bottom" node ($\bot$). Otherwise, according to Wadsworth's theorem (Theorem 8.3.14), M has a head normal form (hnf). But a solvable term may have many hnfs, here we choose the "principle hnf" (the last element of its head reduction path), which may be represent by M := LAMl vs ((VAR y) @* Ms). Then the root of the Böhm tree is nothing but LAMl vs (VAR y) and the children are each terms in the list Ms, translated in the same way as M.

The problem is that, under α-conversion, it's unsound to define any function to directly retrieve VAR y and Ms from the hnf LAMl vs ((VAR y) @* Ms) and then construct LAMl vs (VAR y) as the tree node, because vs as a list of bound variables can be replaced by any other variables, as long as they have no conflict with the free variables of M. My solution is to first pick vs to avoid FV M, and then apply M with MAP VAR vs, and then we got the inner part, since M @@ MAP VAR vs == (VAR y) @* Ms.

The tree data structure is based on ltreeTheory in HOL's core theory. First, a Böhm tree generator is defined in this way: (note that, we represent LAMl vs (VAR y) by (vs,y), thus the type of Böhm tree do not have :term as type arguments, it's all in :string.)

[BT_generator_def]
⊢ ∀X M.
    BT_generator (X,M) =
    if solvable M then
      (let
         M0 = principle_hnf M;
         n = LAMl_size M0;
         vs = FRESH_list n (X ∪ FV M);
         M1 = principle_hnf (M0 ·· MAP VAR vs);
         Ms = hnf_children M1;
         l = MAP ($, (X ∪ set vs)) Ms;
         y = hnf_headvar M1;
         h = (vs,y)
       in
         (SOME h,fromList l))
    else (NONE,[||])

Note that the generator doesn't start with just the input term M. Instead, it takes an extra set of variables X as the excluded set, to make sure that all generated binding variables have no conflict with either FV M and X (see vs = FRESH_list n (X ∪ FV M) in above definition). Further more, in hnfs like LAMl vs ((VAR y) @* Ms), the binding variables vs may occur freely in (VAR y) @* Ms. Therefore, when going into the next level of tree generation, just excluding X (and FV M) is not enough, the vs from current level must be also added too. This is why I have l = MAP ($, (X ∪ set vs)) Ms in the above definition for the tree generation of children in Ms.

Once the ltree generator is ready, the Böhm tree itself is simply defined below:

[BT_def]
⊢ BT = ltree_unfold BT_generator

The Böhm tree of M w.r.t. X is given by BT (X,M) or BTe X M (BTe = CURRY BT). Clearly for each different X the resulting tree is also different. The purpose of this extra set X can be seen by the following "key" theorem saying that two β-equivalent terms have the "same" Βöhm tree:

lameq_BT_cong
⊢ ∀X M N. FINITE X ∧ FV M ∪ FV N ⊆ X ⇒ M == N ⇒ BTe X M = BTe X N

Note that, when M == N, for the conclusion BTe X M = BTe X N to hold, the choice of X is NOT arbitrary: it must contains at least all free variables from M and N. This is because, in the definition of BT_generator, we can easily see that X ∪ FV M = X ∪ FV N if FV M ∪ FV N ⊆ X holds, and thus at each correspond tree levels, the FRESH_list inside BTe X M and BTe X N will literally generate the same binding list vs, rendering the two Böhm trees completely identical.

The second evidence (for the correctness of BT_generator) is the connection of Böhm trees to the similar concept "subterm" (Definition 10.1.13), defined as below:

[subterm_def]
⊢ (∀X M. subterm X M [] = SOME (X,M)) ∧
  ∀X M x xs.
    subterm X M (x::xs) =
    if solvable M then
      (let
         M0 = principle_hnf M;
         n = LAMl_size M0;
         vs = FRESH_list n (X ∪ FV M);
         M1 = principle_hnf (M0 ·· MAP VAR vs);
         Ms = hnf_children M1;
         m = LENGTH Ms
       in
         if x < m then subterm (X ∪ set vs) (EL x Ms) xs else NONE)
    else NONE

The tool "subterm" can access the children term according to a (finite) list of numbers as the "access path". When the list is empty, the subterm of M is M itself. Otherwise, the input term is first translated to its principle hnf, LAMl vs ((VAR y) @* Ms) (if not solvable then there's no subterm, returning NONE), then the path [i] will give us EL i Ms (the i-th element of hnf children Ms. For a deeper path like [1;2], we first get EL 1 Ms and then repeat the process by getting the principle hnf of EL 1 Ms and then access the EL 2 of its hnf children, etc.

We can imagine that subterm X M p is not any node content in the Böhm tree BT(M), because in the tree the node following the same path p is the head part of the principle hnf of subterm M p. But if we try to generate Böhm trees of the subterm, the resulting tree must be a subtree of the original BT(M). The following theorem formalized this observation and make the connection between subterm and BT (or BTe):

BT_subterm_thm
⊢ ∀p X M.
    p ∈ ltree_paths (BTe X M) ∧ subterm X M p ≠ NONE ⇒
    BT (THE (subterm X M p)) = THE (ltree_lookup (BTe X M) p)

Many new utility theorems were added to serve the above results. The previously added ltree_finite_branching has been renamed to just finite_branching (no conflict with other core theories), and we can prove that Böehm trees are always finite branching (but may have infinite depth, thus is coinductive in general):

[BT_finite_branching]
⊢ ∀X M. finite_branching (BTe X M)

The deep connection between Böhm trees and the concept of "Böhm transformations" added in previous PR #1169, is yet to be shown.

[mn200]

Exciting progress!