[examples/lambda] Update documentation in examples/lambda/basics

Author: mn200

examples/lambda/basics/README

@@ -1,26 +1,55 @@
+appFOLDLScript.sml
+   Defines iterated (left-associated) application in Λ so that 
+
+     M @* [M1; M2] = (M @@ M1) @@ M2
+
 basic_swapScript.sml
    Very basic theory of swaps over strings (the swapstr constant), and
    permutations (which take a list of pairs of strings to swap).  Also
    defines the NEW constant, which is used everywhere (including in
-   the dB and nc developments above).
+   the dB and nc developments in other-modesls).
+
+binderLib.{sig,sml}
+   Tools for doing proofs with terms that include binders, including
+   function definition and facilities from NEWLib.
+
+ctermScript.sml
+   Defines a type like Λ(A) with A a set of additional constants,
+   introduced, for example, in Barendregt §5.2. In HOL, the A is a
+   type variable so that we get α cterms with constructors APP, LAM,
+   CONST and VAR.
+
+generic_termsScript.sml
+   Defines a large type of trees with α-equivalent binders over
+   strings that can be used as the basis for the definition of a
+   number of "nominal" types. The genind constant provides a way of
+   encoding a variety of subsets of this type, as described in
+   notes.txt. 
+
+NEWLib.{sig,sml}
+   simple tactics to use with the NEW constant.
+
+nomdatatype.{sig,sml}
+   Some very rudimentary code to provide some automation in the
+   definition of types built from generic_terms (as above). 
 
 nomsetScript.sml
    A more involved theory of permutations and their actions on
    arbitrary types (the "nominal sets").  Includes the notion of
    support.
 
-NEWLib.{sig,sml}
-   simple tactics to use with the NEW constant.
-
-binderLib.{sig,sml}
-   Tools for doing proofs with terms that include binders, including
-   function definition and facilities from NEWLib.
+notes.txt
+   Tries to explain the genind + generic_terms technology for building
+   new types with binders.
 
-pretermScript.sml termScript.sml
-   Using a quotient over raw syntax from pretermTheory, establishes a
-   type of lambda calculus terms, and defines substitution, the notion
-   of free variable and permutations over that type.  Proves some
-   simple lemmas about substitution.  For example,
+termScript.sml
+   Constructs the classic type of lambda terms, with three
+   constructors, called Λ in lots of places. Does this by constructing
+   a subtype of the “generic” terms. Defines various flavours of
+   substitution proves some simple lemmas about these. For example,
 
      lemma14a: |- [VAR x/x] t = t
 
+termSyntax.{sig,sml}
+   Standard HOL-style syntactic support for programmatically
+   manipulating terms of type “:term”.

examples/lambda/basics/notes.txt

@@ -21,6 +21,14 @@ So there are four constructors: the three standard ones, and another one that ta
 
 If you look at the LAMi_def (LAMi is the labelled redex constructor) in that file, you’ll see how the two term arguments get split apart the two lists (one is bound; one is not).  Note that when you have no terms in the bound scope (as happens in APP), you still have to provide a bound variable (ARB in the definitions), but there is a theorem that says all choices of bound variables result in the same g.term (GLAM_NIL_EQ).
 
+The ctermScript.sml example in this directory is yet another example, where the type is characterised by
+
+  Λ(A) ::= v | Λ(A) Λ(A) | cₐ (a ∈ A) | λv. Λ(A)
+
+The CONST constructor corresponding to the cₐ clause above is encoded by a third disjunct in the lp predicate, and by having the GLAM type variable be
+
+   :unit (* APP *) + unit (* LAM *) + α (* CONST *)
+
 The last thing to understand is the vp and lp predicates that restrict the new type to be a subset of the full generic term universe.
 
 These predicates encode the possible shapes of the new recursive type.  See the lp definition at the top of labelledTermsScript:
@@ -32,6 +40,15 @@ These predicates encode the possible shapes of the new recursive type.  See the
 
 This is the predicate specifying what’s allowed in the case of GLAM.  There are three possibilities.  Each picks out one of the possible data forms and then constrains the tns and uns list.  These lists "correspond" to the two list arguments that are passed to GLAM.   The first clause above says that if the data component is an INL, then tns must be empty, and there must be two values in the uns list.  This is encoding APP, which does indeed require two term arguments, but where these are not bound.  The second possibility corresponds to LAM, and insists on one element in tns and none in uns.  The one element of tns corresponds to the one term argument of LAM.  Finally, the third argument corresponds to the LAMi case, where there is a term in each list.
 
+In cterm, the definition is
+
+  val lp = “(λn (d:unit + unit + 'a) tns uns.
+               n = 0 ∧ ISL d ∧ tns = [] ∧ uns = [0;0] ∨
+               n = 0 ∧ ISR d ∧ ISL (OUTR d) ∧ tns = [0] ∧ uns = [] ∨
+               n = 0 ∧ ISR d ∧ ISR (OUTR d) ∧ tns = [] ∧ uns = [])”
+
+where the third clause is there for the CONST constructor: there are no recursive occurrences (subject to binding or otherwise), but there is an α-value required.
+
 Now, finally, why the numbers?  So, this scheme is meant to allow for multiple types to be defined at once, where there’s mutual recursion.  If you do that, you specify different numbers at the head of the clause, and in the sub-lists. I think this will work, and there is an example in
 
   examples/logic/foltypesScript.sml