Automated Reasoning in Higher Order Logic
This page was created and is maintained by Chad E Brown.
Chapter 1: The type-free lambda calculus.
Chapter 2: Assigning types to terms.
Chapter 3: The principal-type algorithm.
Chapter 4: Type assignment with equality.
Chapter 5: A version using typed terms.
Chapter 6: The correspondence with implication.
Chapter 7: The converse principal-type algorithm.
Chapter 8: Counting a type's inhabitants.
Introduction: This book studies the system TA (for "Type Assignment") which is lambda calculus (with variables but no constants) and types built from type variables and arrows. The main results discussed are the principal-type algorithm, the converse principal-type algorithm, and the inhabitant-counting algorithm.
Chapter 1: The type-free lambda calculus. Lambda terms are built from term-variables by application and lambda abstraction. For each lambda term we have notions of length, subterms, occurrences, components, body, scope, covering abstractors (of a subterm [those abstractors which dominate the subterm]), free and bound non-binding variable-occurrences. We also have substitution, alpha-conversion, bound-variable clashes, and closed terms = combinators. The common combinators (including Curry's fixed point combinator Y) are given.
Beta-contraction (one step of a beta-reduction), beta-reduction and beta-conversion are defined. The Church-Rosser Theorem (for beta) proves that if P beta-converts to Q, then there is a T such that P and Q beta-reduce to T. This is shown by first showing [the diamond property] that if M beta-reduces to P and M beta-reduces to Q, then there is a T so that P and Q beta-reduce to T. Then this can be applied to an induction argument to show the theorem.
It follows that a term can have at most one beta-normal form [disallowing eta-convertibility!], modulo alpha-conversion. Leftmost beta-reductions are guaranteed to terminate in a beta-normal form if such a form exists. (That is, the leftmost reduction strategy is normalizing; this follows from the Standardization Theorem.) Furthermore, an induction argument shows that every beta-normal form is of the form "lambda x1 . . . lambda xm . y N1 . . . Nn." If the term is closed, then y must be a member of {x1,...,xn}.
Next, eta-contraction (one step of an eta-reduction), eta-reduction and eta-conversion are defined. All eta-reductions are finite. The eta-family of a term P is the set of all Q such that P eta-reduces to Q. The Church-Rosser Theorem holds for eta. We can combine beta and eta to get beta-eta-reductions and beta-eta-conversions, and we can show that we may perform beta-reduction first, then perform eta-reduction ("eta-Postponement Theorem"), or vice versa ("Commuting Lemma"). Church-Rosser holds for beta-eta. Since beta-normality is preserved under eta-contraction, we can first find the beta-normal form by beta-reduction (if it exists) and then eta-reduce to eta-normal form (which we know terminates) and obtain a beta-eta-normal form. So, a term has a beta-nf iff it has a beta-eta-nf.
Some natural restrictions of lambda calculus include lambda-I-terms (which require that x must occur in M for terms "lambda x M"), BCK-lambda-terms (which require that x occur no more than once in M for terms "lambda x M"), and BCI-lambda-terms/linear-terms (which require that x occur exactly once in M for terms "lambda x M"). Each of these classes is closed under beta-eta-reduction (not for expansion of course). Some beta-reductions "cancel" arguments (if the bound variable did not occur in the scope) and others "duplicate" arguments (if the bound variable occurs more than once in the scope). "A beta-reduction is non-duplicating if none of its contractions duplicates, and is non-cancelling if none cancels."
Chapter 2: Assigning types to terms. The Church and Curry approaches to typing lambda terms are contrasted. The Church approach involves restricting the formation of lambda terms to those which a well-typed (so a term such as "lambda x . x x" ["self-application"] would not be in the system at all, and there is no single identity term). The Curry approach starts with all untyped lambda terms and uses rules to assign types to these terms, if possible. TA uses the Curry approach (although Curry actually worked in Combinatory Logic). Whenever we write "M:tau" where M is a term and tau is a type, M is the "subject" and tau is the "predicate". A natural deduction system for proving formulas of the form "Context |-> Term:Type" is given, and we say "Gamma |- M:tau" for a context Gamma, term M, and type tau, if for some context Gamma' subset of Gamma, there is a proof of "Gamma' |-> M:tau." So, |- has the weakening property, but |-> does not. In fact, if we can deduce "Gamma |-> M:tau," then Subjects(Gamma) must contain precisely the free variables in M.
The subject-construction theorem states that given any deduction of "Gamma |-> M:tau," if we erase contexts and predicates, then the resulting tree is simply the construction of the untyped term M. This does not quite imply that deductions are unique (only that their structure is, in some sense, unique) because types may be introduced and eliminated before the end of the deduction. However, for beta-nf's M, any deduction of "Gamma |-> M:tau" is unique (because every type appearing in the proof must be a type in Gamma or occur in tau). This corresponds to the subformula property in Natural Deduction (think of the Curry-Howard correspondence).
Typability is invariant under alpha-conversion, and we can perform well-typed substitutions (assuming the appropriate contexts are consistent).
The subject-reduction theorem states that if Gamma |- P:tau and P beta-eta-reduces to Q, then Gamma |- Q:tau. The subject-expansion theorem states that if Gamma |- Q:tau, and P beta-reduces [note: no eta!] to Q by non-duplicated, non-cancelling contractions, then Gamma |- P:tau. (In general, beta-expansion may destroy typability altogether--consider "[lambda x . x x] I." Also, even if both P and Q are typable where P beta-reduces to Q, Q may have more types than P.) For closed terms P, let Types(P) be the set of types tau so that |- P:tau (note empty context). So, if P beta-reduces to Q, then Types(P) is a subset of Types(Q), with equality if the beta-reduction is non-duplicating and non-cancelling.
The class of (TA-)typable terms is closed under subterms, beta-eta-reduction, non-cancelling and non-duplicating beta-expansion, and lambda-abstraction. This class is decidable (the principal-type algorithm in the next chapter provides not only a decision procedure but a calculation of the most general type of a term if one exists). For TA-typable terms we have not only Weak Normalization (WN--every term has a beta-nf and a beta-eta-nf), but Strong Normalization (SN--every beta-eta-reduction is finite). It follows that beta-eta-convertability is decidable.
All BCK-lambda-terms are typable (because there are no multiple occurrences of variables).
Chapter 3: The principal-type algorithm. First, we can define a notion of substitution for type variables applied to types, contexts, formulas, and deductions. A principle type (PT) of a term M is one so that "Gamma |- M:tau" for some Gamma and so that sigma is an instance of tau if [and only if follows] "Gamma' |- M:sigma" for some Gamma'. (Gamma,tau) is a principal pair in this situation. A principal deduction for a term M is one so that any other deduction for a term M is an instance. Any principal deduction is a deduction of a principal type. The Principal Type (PT) Theorem states that every typable term has a principal deduction, hence a principal type, in TA. Also, there is an algorithm given which depends on unification for types. (Such an algorithm [for CL] was used informally by Curry in the 1950's; a PT algorithm [for CL] depending on Robinson's [1965] unification algorithm [which Curry's algorithm did not] was given by Hindley [1969] and it is this algorithm which forms the basis of the one given in this book. The first PT-algorithm for lambda-calculus was due to Morris [1968]; this did not call an external unification algorithm.)
First, the theory of type-substitutions is developed. The following concepts are defined: empty substitution, single substitution, component (and trivial component), nontrivial kernel, domain (substitutions are treated as total functions acting as the identity on variables outside the domain), range, extensional equality (which may differ from equality due to trivial components), restriction, union (of compatible type-substitutions), composition (s o t, where Dom(s o t) is Dom(t) union [Dom(s) - Dom(t)]), variables-for-variables substitution, renamings, inverses, and alphabetic variants. Basic results are proven, including the Composition-extension Lemma which states that if r, s, and t are substitutions with Dom(r) disjoint from Dom(s) and Dom(t) and Range(t), then both "r union (s o t)" and "(r union s) o t" are defined and are equal.
The idea for the PT algorithm is roughly as follows: To type [P Q] where PT(P) = rho -> sigma and PT(Q) = tau, we need to find the most general common instance [differs from unifier by treating variables in sigma and tau as distinct] of sigma and tau. We have to be careful not to accidentally identify variables by using alphabetic variants. We must keep in mind that P and Q may share term-variables (which must end up with the same types). Also, there is the special case where PT(P) is a type variable.
The problem of finding most general common instances can be reduced to the problem of finding most general unifiers (both of which are unique up to renaming of variables). Robinson's Unification Algorithm for a pair of sequences of the same length [find the first disagreement pair and use it to assign a variable to a term or fail] is given and proven correct.
Once we have unification, the PT algorithm can be given in detail and proven correct. In the base case we have a variable and the principle type is a type-variable. In the first and second inductive cases we have PT([lambda x P]) we find PT(P) = beta [or fail] where x may or may not be free in P. If x is free in P, then x is assigned a type alpha in Gamma in the principal deduction of "Gamma |-> P:beta" and PT([lambda x P]) = alpha->beta. If x is not free in P, then we assign x to have type d where d is a fresh type-variable, and PT([lambda x P]) = d -> beta. In the last case, we have PT([P Q]). In the first subcase, PT(P) = sigma -> rho and PT(Q) = tau. Here we find the most general unifier of sigma and tau (and the types of term-variables common to P and Q), and apply the substitution to rho to find PT([P Q]). In the second subcase PT(P) = b where b is a type-variable and PT(Q) = tau, we apply unification to b and tau -> c (where c is a fresh type-variable) and the types of the common term-variables and use this to find PT([P Q]) as the substitution value of c.
Chapter 4: Type assignment with equality. We can extend the type assignment system TA by including rules so that beta-[eta-]convertibility preserves type assignments. The resulting systems do not satisfy the subject-construction theorem, but we can postpone the beta-[eta-]equality inference rule until the last step. Weak normalization follows, but strong normalization does not. Weak normalization implies that the typable terms in such systems are precisely those which have a beta-nf. Furthermore, the principal type of such a terms is the principal type of its beta-[eta-]nf. These type assignment systems are undecidable, since a decision procedure would allow us to decide the class of untyped lambda terms which are beta-[eta-]convertible to I.
A natural semantics follows for these systems. The concepts of lambda-model and extensional lambda-model are defined. Types are interpreted as subsets of the domain of the model (called "simple semantics"). A term model can be built and used to show soundness and completeness. (Other models which have been used to show completeness include a filter model [Barendregt 1983] and the graph model P(omega) [Coppo 1984].) TA can also be given a semantics based on reduction instead of equality [Plotkin 1994].
Chapter 5: A version using typed terms. A typed-term language can be introduced to encode TA deductions in a compact manner. Such a language differs from the Church approach in the important respect that terms are only typed within a context, as opposed to variables having a global type assignment in the Church approach. The result is that the set of typed terms TT(Gamma) within a fixed context Gamma is not closed under subterms and that M:sigma->tau and N:sigma can only be combined through application if the corresponding contexts are consistent. Every typed term is also a typed term in a minimum context (restricting Gamma to the free variables in the term). The translation between deductions and typed terms is given.
Replacement of subterms of typed terms is defined under certain restrictions on the contexts. (These conditions play a role in proofs later in the book.) One restriction is that the context of the new subterm is a subcontext of the context of the original subterm. An alternative restriction is that the context of the new subterm union with the context of the full term union with the context given by the bound variables in whose scope the subterm lies is consistent. These conditions ensure consistency of the appropriate contexts so that the replacement can be made giving a well-defined typed term.
The notion of a bound-variable clash can be defined using the same notion for untyped terms using type erasure. Then, typed substitution for beta-redex's with no bound-variable clashes can be defined, building in alpha-conversion to avoid capture. Alpha-conversion, beta-reduction, and eta-reduction can be defined for typed terms (but we avoid considering beta-expansion since this may not preserve typability). The Church-Rosser Theorem holds (using the same style of proof). We have Weak Normalization of beta and beta-eta [Turing 1942, Curry/Feys 1958] by induction on the maximum degree of beta-redex's, where the degree of [[lambda x:sigma M:tau] N:sigma] is the number of atom-occurrences in the type sigma->tau. Note the similarity of this proof to the one in Andrews 1971 that typed lambda terms (in the Church approach) have normal forms. Using the Curry-Howard correspondence, this is seen to be related to Gentzen's cut-elimination. We also have Strong Normalization.
Chapter 6: The correspondence with implication. We can show a Curry-Howard correspondence between TA and intuitionist implicational logic. Natural deduction for such a logic can be defined in a way structurally similar to type assignment deductions, where the formulas correspond to types. The assumptions which are discharged correspond to which variables are bound at a lambda abstraction. Given any TA deduction of {x_1:rho_1,...,x_n:rho_n} |-> M:tau, we can erase the subjects and contexts and add the discharge position information to obtain a natural deduction of rho_1, . . ., rho_n |- tau. Since some of the x_i may have the same types, different TA deductions may map to the same logic deduction. However, we can define a one-sided inverse by taking a natural deduction proof of rho_1, . . ., rho_n |- tau and building a TA deduction of {x_1:rho_1,...,x_n:rho_n} |-> M:tau choosing x_i to be distinct whenever possible. The correspondence is 1-1 (modulo alpha-conversion) if we restrict ourselves to provability (deducibility from no assumptions) which corresponds to closed terms. So, we can decide if an implicational formula tau is provable in Intuitionistic logic by deciding if there is a closed typed term with type tau. In fact, we can count the "irreducible" proofs by counting the closed beta-nf's with type tau. As a result, we can prove (using SN and a result in Chapter 8 that no closed normal form has the appropriate type) that Peirce's Law "((a -> b) -> a) -> a" is not provable in Intuitionistic logic.
Restricted classes of lambda-terms correspond to restricted logics. Relevance logic (no vacuous discharging allowed) corresponds to closed lambda-I terms. BCK-logic (no multiple discharging allowed) corresponds to closed BCK-lambda-terms. BCI-logic (no multiple or vacuous discharging allowed) corresponds to BCI-lambda-terms.
Finally we can consider the correspondence with Hilbert-style Axiom-based systems. (The original correspondence was between such systems and CL.) Such a system has a set of axioms A and two inference rules: ->E (modus ponens/detachment) and Sub (with the restriction that the variables being instantiated do not occur free in any non-axiom assuption upon which the line depends). Every deduction in such a system can be replaced by a "substitutions-first" deduction, in which Sub is only applied to axioms (so that the restriction on Sub is automatically satisfied). Hilbert-style Intuitionist logic, relevance logic, BCK-logic, and BCI-logic are defined. The axioms of each system correspond to the principal types of certain combinators. Intuitionist logic corresponds to the types of B, C, K and W. Relevance logic corresponds to B, C, I, and W. BCK-logic corresponds to B, C and K. BCI-logic corresponds to B, C, and I. The theorems of each logic are precisely the types of the applicative combinations of the appropriate combinators. The derivability relation corresponds to applicative combinations allowing variables of the types in the assumption. This is because Sub corresponds to the fact that if we can prove Gamma |-> M:tau, then we can prove all instances, and because ->E (modus ponens) corresponds to application. Also, the fact that we do not have ->I (as in natural deduction) corresponds to the fact that we do not allow abstraction.
Moral: Hilbert-style Deduction <--> Combinatory Logic
Gentzen Natural Deduction <--> Lambda Calculus
The well-known correspondence between Combinatory Logic and Lambda Calculus provides a correspondence between Hilbert-style Deduction and Gentzen's Natural Deduction. The deduction (meta-)theorem of Hilbert-style systems corresponds to combinatory completeness of Combinatory Logic.
Chapter 7: The converse principal-type algorithm. Given a type tau which can be assigned to a closed term M, there is an algorithm which yields a closed term M* which beta-reduces to M and has principal type tau (proven by constructing terms I_sigma:sigma->sigma for every sigma which beta-reduces to I and letting M* = [I_sigma M]). This implies that we can find closed terms P and P' which both beta-reduce to I, but have no types in common. For the lambda-I calculus (corresponding to relevance logic), if M is a closed lambda-I term which can be assigned type tau, then there is an algorithm which yields a closed lambda-I term M* which beta-eta-reduces to M and has principal type tau.
To prove the latter statement, we must first define the notions of "identification" [of type-variables in a type] and "skeletal" [types in which no type-variables has multiple occurrences]. By induction, for each skeletal type theta we can construct lambda-I terms I_theta so that I_theta beta-eta-reduces to I and theta->theta is the principal type of I_theta. So, given tau* the skeleton of type tau, where |- M:tau, we can let M+ = [I_tau* M]. M+ beta-eta-reduces to M and a sequence of identifications on tau+ = PT(M+) gives tau. A single-replacement lemma and a double-replacement lemma are proven which allow us to replace one or two type variables in a skeletal type using a lambda-I term. These are used to show the Identification Lemma which allows us to identify two type-variables in a principal type and obtain another principal type (the trick is to take the original type tau, form the skeletal type tau*, choose an occurrence of the two type-variables [a1 and b1, say] to be identified and replace them with new type-variables [using Double Replacement] giving tau' [skeletal] and a closed lambda-I term R with PT(R) = (a1->f)*->(b1->g)*->(tau*->tau') and finally form the term N = [lambda x . R x x] I M which beta-eta-reduces to M and requires a1 and b1 [and all other occurrences of a and b] to be identified). So, given |- M:tau for a lambda-I term, construct M+ and tau+ as above so that tau can be obtained by a sequence of identifications. Then perform each identification as above, giving the result.
Actually, in terms of Combinators, Meyer and Bunder [1988] showed that every type of a BB'IW-combination is also a BB'IW principal type. The above proof is a lambda-adaptation of this proof.
In terms of provability in implicational calculi, the Converse Principal Type Theorem implies completeness of a "condensed detachment" rule "Rule D" which combines modus ponens and Sub [in the style of resolution with unification] (as developed by Carew and David Meredith independently of principal types). In particular, D-completeness follows for full intuitionist implicational logic and for relevance logic. In fact (in terms of Hilbert-style axiomatic deduction), if A is D-complete and a->a is an A-theorem and the set of all D-theorems from B includes all D-theorems of A, then B is D-complete. This is the D-extension lemma. This gives completeness for classical logic (as given by the axiom-set {B,C,K,W} for intuitionism plus Peirce's law "((a->b)->a)->a").
Examples of D-incomplete axiom-sets are {B,C,K} [giving linear logic] and {B,C,I} [linear + relevance]. By D-extension, it is enough to prove this for {B,C,K}. Here, D-incompleteness is proven by showing that "((a->a)->a)->a" is a theorem, but cannot be a D-theorem, because if it were a D-theorem then it would be the principal type of some applicative combinations of {B,C,K}, say M. Since MI would be a BCK-term [linear], it would be typable. However, finding the principal type of MI would involve unifying "(a->a)->a" with "rho->rho" which fails to unify.
Note that D-completeness is a property of a set of axioms, not the logic generated.
Chapter 8: Counting a type's inhabitants. An inhabitant of a type tau is a closed untyped term M such that |- M:tau (or a closed typed term M^tau, which amounts to the same thing by the correspondence between typed terms and TA-deductions). There are algorithms [Ben-Yelles] which can decide if the number of normal inhabitants of a type is finite or infinite, and list them (this enumeration will continue forever if the number of normal inhabitants is infinite). We consider long closed typed beta-nf's M^tau. Since eta-reductions are finite, these long forms generate a finite family of eta-equivalent beta-nf's, including one in beta-eta-nf. Also, for every beta-nf there is a unique eta-equivalent long beta-nf (up to alpha-convertibility). The family of beta-normal inhabitants of tau is infinite iff the family of beta-eta-normal inhabitants of tau is infinite.
We can also consider principal and normal principal inhabitants (those terms whose principal type is tau). Note that since PT(.) is not strictly preserved under reduction, a type may not have normal principal inhabitants. The converse principal types theorem implies that if a type has any inhabitants, it has a principal inhabitant.
A type tau = "t1 -> . . . -> tm -> e" has "premises" (the occurrences of) t1,...,tm and "conclusion" (or "tail") (the occurrence of) e. Closed long beta-nf's of type tau must have the form "lambda x1 . . . lambda xm . xi M^1 . . . M^n" where the conclusion of the type ti of xi must be e. These restrictions are enough to show that S is the only normal inhabitant of the type "(a->b->c)->(a->b)->a->c." Also, the type "a ->. . . -> a -> a" (with m+1 a's) has exactly m normal inhabitants (the projections). Examples of types with no inhabitants are atomic types, skeletal types, and Peirce's Law "((a->b)->a)->a."
The general search algorithm constructs long beta-nf-scheme's (with meta-variables) of type tau increasing the depth by one at each step by replacing meta-variables with suitable replacements with either a depth 0 term with no new meta-variables or a depth one scheme with new meta-variables. These suitable replacements depend upon what variable we use for the head [either projection by using a variable from the initial abstractor or imitation by using a variable in whose scope the meta-variable lies].
If we let D(tau) = |tau| x ||tau|| where |tau| is the number of atom-occurrences in tau and ||tau|| is the number of distinct atoms in tau, then we have two important lemmas which allow us to distinguish, in finite time, whether the family of normal inhabitants is finite or infinite. The Stretching Lemma implies that if there is a long beta-nf of type tau and depth greater than ||tau||, then the family of normal inhabitants of tau is infinite. (The idea of the proof is that there must be some components B and C of the same type, with C inside B. We can construct another long beta-nf by replacing C with B. This process can be continued indefinitely, giving arbitrarily deep long beta-nf's of type tau.) The Shrinking Lemma implies that if there is a long beta-nf of type tau of depth >= D(tau), then there is a long beta-nf N of type tau with D(tau) - ||tau|| <= Depth(N) < D(tau).
So, we can perform the search algorithm to depth D(tau). If there are no inhabitants (term-schemes with no meta-variables) generated, then by the Shrinking Lemma, there must be no inhabitants of tau. If there is an inhabitant of depth >= ||tau||, then by the Stretching Lemma, there must be infinitely many inhabitants. Otherwise, the number of inhabitants are finite and have been generated (or are eta-equivalent to those generated).
A monatomic type tau (i.e., ||tau|| = 1) of the form "tau_1 -> . . . -> tau_n ->a" falls into one of the cases: 1.) Some tau_i is composite and the number of normal inhabitants is infinite or zero, or 2.) All tau_i are a and the n projection functions are the only normal inhabitants.
Problems related to counting principal inhabitants and principal normal inhabitants and inhabitants in restricted classes of terms are still open.
The efficiency of the counting algorithm cannot be any better than P-space, since the decision problem for intuitionist logic can be reduced to the counting problem, and Statman [1979] showed the decision problem for intuitionist logic is P-space complete.
The final two sections of this chapter works out the technical details to prove the Stretching and Shrinking Lemmas and the completeness of the search algorithm.
Chapter 9: Technical details. This chapter is dedicated to working out details for certain concepts which were treated intuitively in earlier chapters. First, occurrences, components, and replacement in terms are defined by defining positions (as strings of *, 0, 1, 2) and using these to make the notion of construction of a term precise.
Next, residuals of a beta-redex with respect to a beta-reduction are defined. This leads to "complete developments" (in which we start with some beta-redex-occurrences and perform the corresponding beta-reductions [sometimes on residuals from previous beta-reductions]) and "minimal complete developments" (in which we ensure that the beta-reduction performed does not contain beta-redexes from the set of redex-occurrences). Every set of redex-occurrences has a minimal complete development. In order to beta-normalize, however, we must also consider newly created redex-occurrences. A beta-redex may be created in, essentially, two ways. The first is a situation like "[lambda x [lambda y A] B C]." The second is a situation like "[lambda x . x M] [lambda y H]."
A TA-deduction is defined with position markers (strings from 0, 1, 2). This allows us to be precise about replacement. Positions are used similarly (string from 1, 2) to make occurrences of subtypes in a (construction-tree of a) type tau precise. These also allow us to define positive and negative occurrences in a type.
This structure of a type may be modified from being a binary construction-tree to allow larger branching so that a type "tau_1 -> . . . -> tau_m -> e" is has m+1 branches using numbers (m, . . . ,1) for the premise type occurrences tau_1, . . ., tau_m and * for the tail occurrences of e. This allows us to define s-subtypes ("significant subtypes") and s-components which, for the example above would include each tau_i, e, and the whole type, but would not include "tau_m -> e" (unless, of course, m = 1). The idea is that we are not considering the type as a Curried unary function, but an m-ary function. Next, we define subpremises and subtails (only considering s-components). The number of subtails of tau is <= |tau| -1, and the number of subpremises of tau is |tau| -1. As a result, the number of s-components of tau is <= 2|tau| - 1. The order of tau is 1 for atoms and 1 + Max(Order(premises of tau)) for component types. Finally, the set of "Negative subpremise-sequences" is defined. The number of such sequences, and the number of types used in the sequences, and the length of the sequences are all bounded by |tau| - 1. These concepts and bounds are used to prove the Shrinking Lemma in Chapter 8.
Finally, we can perform combinatory logic within lambda calculus by defining the usual combinators in the usual ways. Combinatory Completeness is proven, i.e., that there is an algorithm which constructs from a lambda-term M a BCKW-and-variables term M* which beta-reduces to M and so that FV(M*) = FV(M) and Types(M*) = Types(M). [Note: I can be defined as CKK.] A typable basis for a set L of lambda-terms is a set S of typable closed lambda-terms so that there is an algorithm as described above for all lambda-terms M in L. So, the theorem proves that {B,C,K,W} is a typable basis for all lambda-terms. By modifying the proof in straightforward ways, we have {B,C,I,W} is a typable basis for lambda-I-terms [relevance]; {B,C,K} is a typable basis for BCK-lambda-terms [linear]; and {B,C,I} is a typable basis for BCI-lambda-terms [relevance + linear].