Combinatory Logic

First published Fri Nov 14, 2008; substantive revision Tue Nov 5, 2024

Combinatory logic (henceforth: CL) is anelegant andpowerful logical theory that is connected to many areas oflogic, and has found applications in other disciplines, especially, incomputer science and mathematics.

CL was originally invented as a continuation of the reduction of theset of logical constants to a singleton set in classical first-orderlogic (FOL). CL untanglesthe problem of substitution, becauseformulas can be prepared for theelimination of bound variablesby inserting combinators. Philosophically speaking, an expression thathas no bound variables represents the logical form of the originalformula. Sometimes, bound variables are thought to signify “ontological commitments.” Another philosophical rôle of CL is to show the variability ofthe ontological assumptions a theory has.

Substitution is a crucial operation not only in first-order logics,but also inhigher-order logics, as well as in other formal systems that contain a variable bindingoperator, such as the $\lambda$-calculuses and the$\varepsilon$-calculus. Indeed, carrying out substitution correctlyis particularly pressing in$\lambda$-calculuses and in the closely related functional programming languages. CL canemulate $\lambda$-abstraction despite the fact that CL has novariable binding operators. This makes CL a suitable target languagefor functional programming languages to be compiled into.

The connection to $\lambda$-calculuses mightsuggest—correctly—that CL is sufficiently expressive toformalizerecursive functions (i.e.,computable functions) and arithmetic. Consequently, CLis susceptible toGödel-type incompleteness theorems.

CL is an archetypicalterm rewriting system (TRS). Thesesystems comprise a wide range of formal calculuses from syntacticspecifications of programming languages and context-free grammars toMarkov algorithms; even some number theoretic problems may be viewedas special instances of questions about TRSs. Several notions andproof techniques that were originally invented for CL, later turnedout to be useful in applications to less well-understood TRSs.

CL is connected tononclassical logics via typing. First, acorrespondence between formulas that are provable in the implicationalfragment of intuitionistic logic and the typable combinatory terms wasdiscovered. Then the isomorphism was generalized to other combinatorybases and implicational logics (such as the logic of relevantimplication, exponential-free linear logic, affine logic, etc.).

Self-reference factors into some paradoxes, such as the widelyknownliar paradox andRussell’s paradox. The set theoretical understanding of functions also discourages theidea of self-application. Thus it is remarkable that pure untyped CLdoes not exclude the self-application of functions. Moreover, itsmathematical models showed that a theory in which functions can becometheir own arguments is completely sensible, in addition to beingconsistent (what was established earlier using proof theoreticmethods).

1. Schönfinkel’s elimination of bound variables

1.1 The problem of substitution

Classical first-order logic includesquantifiers that aredenoted by $\forall$ (“for all”) and $\exists$(“there is a”). A simple sentence such as “All birdsare animals” may be formalized as $\forall x(Bx\supset Ax)$,where $x$ is a variable, $B$ and $A$ are one-place predicates,and $\supset$ is a symbol for (material) implication. Theoccurrences of the variables in the closed formula $\forallx(Bx\supset Ax)$ arebound, whereas those in the open formula$Bx\supset Ax$ arefree. If we assume that $t$ (for“Tweety”) is a name constant, then an instance of theabove sentence is $Bt\supset At$, that may be read as “Tweetyis an animal, provided Tweety is a bird.” This illustrates thatthe instantiation of a (universal) quantifier involvessubstitution.

Due to the simplicity of the example, thesubstitution of $t$for $x$ in $Bx$ and in $Ax$ seems to be easy to understand andto perform. However, a definition of substitution for FOL (and ingeneral, for an abstract syntax, that is, for a language with avariable binding operator) has to guarantee thatno freeoccurrence of a variable in the substituted expressionbecomesbound in the resulting expression.

To see what can go wrong, let us consider the (open) formula $\forallx(Rxy\land Rxr)$, where $R$ is a two-place predicate, $r$ is aname constant abbreviating “Bertrand Russell” and$\land$ is conjunction. $\forall x(Rxy\land Rxr)$ contains a freeoccurrence of $y$ (that is, $y$ is a free variable of theformula), however, $y$ is not free for a substitution of a term thatcontains a free occurrence of $x$, for instance, $x$ itself. Moreformally, the occurrence of $y$ in the second argument place of$R$ in $\forall x(Rxy\land Rxr)$ is not bound by a quantifier (theonly quantifier) of the formula, whereas $\forall x(Rxx\land Rxr)$is a closed formula, that is, it contains no free occurrences ofvariables. Informally, the following natural language sentences couldbe thought of as interpretations of the previous formulas.“Everybody reads him and Russell,” (where‘him’ is deictic, or perhaps, anaphoric) and“Everybody reads himself and Russell.” Obviously, themeanings of the two sentences are vastly different, even if we assumethat everybody pens something. As a contrast, $\forall x(Rxw\landRxr)$ exhibits an unproblematic substitution of the name constant$w$ for the free occurrence of $y$. (The latter formula, perhaps,formalizes the sentence “Everybody reads Ludwig Wittgenstein andBertrand Russell.”) These examples are meant to demonstrate themore complex part of the problem Moses Schönfinkel set out tosolve, and for what he invented CL.^[1]

1.2 The operators “nextand” and “$U$”

A well-known result aboutclassical sentential logic (SL) isthat all truth-functions can be expressed in terms of $\lnot$ and$\land$ (or of $\lnot$ and $\lor$, etc.). A minimal sufficientset of connectives, however, can contain just one connective such as$\mid$ (“nand,” which is often called, Sheffer’sstroke), or $\downarrow$ (“nor,” which is Peirce’sjoint denial). “Nand” is “not-and,” in otherwords, $A\mid B$ is defined as $\lnot(A\land B)$, where $A$,$B$ range over formulas and $\lnot$ isnegation. Going intothe other direction, if $\mid$ is a primitive, then $\lnot A$ isdefinable as $A\mid A$, and $A\land B$ is $(A\mid B)\mid(A\midB)$. Although formulas with numerous vertical lines may quicklybecome visually confusing and hard to parse, it is straightforward toprove that $\mid$ alone is sufficiently expressive to define all thetruth-functions.

Schönfinkel’s aim was to minimize the number of logicalconstants that are required for a formalization of FOL, just as HenryM. Sheffer (indeed, already Charles S. Peirce) did for classicalpropositional logic. One of the two quantifiers mentioned abovesuffices and the other may be assumed to be defined. Let us say,$\exists x A$ is an abbreviation for $\lnot\forall x\lnot A$. Evenif $\lnot$ and the rest of the connectives are traded in for$\mid$, two logical constants remain: $\forall$ and $\mid$. Afurther pressing issue is that quantifiers may be nested (i.e., thescope of a quantifier may fully contain the scope of anotherquantifier), and the variable bindings (that could be visualized bydrawing lines between quantifiers and the variables they bind) may getquite intertwined. Keeping for a moment the familiar logicalconstants, we may look at the following formula that hints at theemerging difficulties—when the question to be tackled isconsidered in its full generality.^[2]

\[\forall x(\exists y(Py\land Bxy)\supset\exists y(Py\land Bxy\land \forallz((Rz\land Ozy)\supset \lnot Cz)))\]

$\forall x$ binds all occurrences of $x$; the variables in thesecond argument place of the two $B$s are bound by one of the two$\exists y$s, the latter of which interacts with $\forall z$ via$Ozy$.

Predicates have a fixed finite arity in FOL, and nothing precludesbinding at once a variable in the first argument of one predicate andin the second argument of another predicate. (Indeed, FOL would losesome of its expressiveness, if bindings of this sort would be excludedwithout some means to compensate for them.) These difficulties persistwhen a formula is transformed into a(n equivalent) formula inprenex normal form. As long as the variable bindings caninterweave and braid into arbitrarily complex patterns, there seems tobe no way to eliminate bound variables. (Note that free variables inopen formulas—in a sense—behave like local name constants,and their elimination is neither intended, nor achieved in theprocedures described here.)

Schönfinkel’s ingenuity was that he introduced combinatorsto untangle variable bindings. Thecombinators $\textsf{S}$,$\textsf{K}$, $\textsf{I}$, $\textsf{B}$ and $\textsf{C}$ (incontemporary notation) are his, and he established that $\textsf{S}$and $\textsf{K}$ suffice to define all the other combinators. Ineffect, he also defined an algorithm to carry out the elimination ofbound variables, which is essentially one of the algorithms usednowadays to definebracket abstraction in CL.^[3]

Schönfinkel introduced a new logical constant $U$, thatexpresses thedisjointness of two classes. For instance,$UPQ$ may be written in usual FOL notation as $\lnot\existsx(Px\land Qx)$, when $P$ and $Q$ are one-place predicates. (Theformula may be thought to formalize, for instance, the naturallanguage sentence “No parrots are quiet.”) In the processof the elimination of the bound variables, $UXY$ is obtained from anexpression that contains ‘$Xx$’ and‘$Yx$’, where $x$ does not occur in $X$ or $Y$.For example, if $X$ and $Y$ happen to be $n$-ary predicates with$n\ge2$, then $x$ occurs only in their last argument places.“Nobody reads Aristotle and Plato” can be formalized as$\lnot\exists x(Rxa\land Rxp)$, where $a$ and $p$ are nameconstants that stand for “Aristotle” and“Plato,” respectively. This formulacannot bewritten as $U(Ra)(Rp)$. On the other hand, “There is nobodywhom both Russell and Wittgenstein read,” that is,$\lnot\exists x(Rrx\land Rwx)$ turns into $U(Rr)(Rw)$, where theparentheses delineate the arguments of $U$. Often, the expressions$X$ and $Y$ (in $UXY$) consist of predicates (and nameconstants)together with combinators and other $U$s.

It is useful to have a notation for “nextand” (i.e.,“not-exists-and”) without assuming either that $x$ has afree occurrence in the expressions joined, or that if it has one, thenit is the last component of the expressions. FollowingSchönfinkel, we use $\mid^x$ for the “nextand”operator that binds $x$. (The notation $\mid^-$, where$^-$ is the place for a variable, closely resembles the Shefferstroke.) Schönfinkel achieved his goal of the reduction of theset of logical constants for FOL to asingleton set$\{\mid^-\}$, because every formula of FOL is equivalent to aformula that contains only “nextand.”

A formula $\forall x A$ is usually defined to be well-formed in FOLeven if $A$ has no free occurrences of $x$. Then, of course,$\forall x A$ is equivalent to $A$ as well as to $\exists x A$,and such quantifiers are calledvacuous. In order to show thatany formula can be rewritten into an equivalent formula that containsonly “nextand,” it is sufficient to inspect the followingdefinitions for $\lnot$, $\lor$ and $\forall$ (with suitablevariables)—that are due to Schönfinkel.

\[\begin{align*}\lnot A & \Leftrightarrow_\textrm{df} A\mid^x A \\A\lor B & \Leftrightarrow_\textrm{df} (A\mid^yA)\mid^x(B\mid^yB) \\\forall xAx &\Leftrightarrow_\textrm{df} (Ax\mid^yAx)\mid^x(Ax\mid^yAx)\end{align*}\]

The definition for $\lnot$, for instance, may be justified by thefollowing equivalences. $A\Leftrightarrow A\land A$, $A\landA\Leftrightarrow \exists x(A\land A)$ (assuming that $x$ is notfree in $A$), hence by replacement, $\lnot A\Leftrightarrow\lnot\exists x(A\land A)$.

Now we give a concrete example to illustrate how to turn a formula ofFOL into one that contains only $\mid^-$, and then how to eliminatethe bound variables using $U$ and combinators. To put someexcitement into the process, we start with the sentence in (#1).

(#1): For every natural number there is a greater prime.

A straightforward formalization of this sentence—on theforeground of the domain of numbers—is the formula in (#2),(where ‘$Nx$’ stands for “$x$ is a naturalnumber,” ‘$Px$’ stands for “$x$ is aprime” and ‘$Gxy$’ is to be read as “$x$is greater that $y$”).

(#2): $\forall y\exists x(Ny\supset(Px\land Gxy))$

This formula is equivalent to $\forall y(Ny\supset\exists x(Px\landGxy))$ and further to $\lnot\exists y\lnot(Ny\supset\existsx(Px\land Gxy))$. In one or two more steps, we get$Ny\mid^y(Px\mid^xGxy)$. (Expressions are considered to begrouped to the left unless parentheses indicate otherwise.E.g., $Gxy$ is $((Gx)y)$ not $G(xy)$ as could have been,perhaps, expected based on the most common way of arrangingparentheses in FOL formulas.) Unfortunately, neither $\mid^x$ nor$\mid^y$ can be replaced by $U$ in the last expression. However,if the arguments of $G$ were permuted then the former reductioncould be carried out. One of the combinators, $\textsf{C}$ doesexactly what is needed: $Gxy$ can be changed to $\textsf{C}Gyx$(see the definition of combinators in section 2.1). That is, we have$Ny\mid^y(Px\mid^x\textsf{C}Gyx)$, and then $Ny\mid^yUP (\textsf{C}Gy)$.^[4] The expression may give the impression that $y$ is the lastcomponent of $UP(\textsf{C}Gy)$, which is the second argument of$\mid^y$, but it is not so. The grouping within expressions cannotbe disregarded, and another combinator, $\textsf{B}$ is needed toturn $UP(\textsf{C}Gy)$ into the desired form$\textsf{B}(UP)(\textsf{C}G)y$. From$Ny\mid^y\textsf{B}(UP)(\textsf{C}G)y$, we get $UN(\textsf{B}(UP)(\textsf{C}G))$ in one more step. This expression is completely freeof variables, and it also makes therenaming of bound variablesin FOL easily comprehensible: given two sequences of (distinct)variables that are different in their first two elements, the reversalof the above process yields formulas that are (logically equivalent)alphabetic variants of the formula in (#2).

The expression $UN(\textsf{B}(UP)(\textsf{C}G))$ may look“unfamiliar” when compared to formulas of FOL, butnotation—to a large extent—is a matter of convention. Itmay be interesting to note that the first $U$ is simply followed byits two arguments, however, the second $U$ is not.$\textsf{B}(UP)$ is a subexpression, but $UP(\textsf{C}G)$ is nota subexpressions of $UN (\textsf{B}(UP)(\textsf{C}G))$. Furthermore,the whole expression can be transformed into $XNPG$ usingcombinators, where $X$ is composed of $U$s and combinators only.Such an $X$ concisely encodes thelogical form orlogicalcontent of the formula with the predicates being arguments.^[5]

The expressions obtained via the transformations outlined abovequickly become lengthy—as trying to rewrite a simple FOLsentence such as $\exists x(Px\land Qx)$ can show.^[6] However, this does not diminish the importance ofSchönfinkel’s theoretical results. A slight increase (ifany) in the length of the expressions is not even an inconvenience,let alone an impediment in the era of computers with petabytes (oreven exa- and zettabytes) of memory.

It seems unfortunate that Schönfinkel’s reduction procedurefor FOL is not widely known, despite the recent publication of Wolfram(2020). This book was written to celebrate the 100-year anniversary ofSchönfinkel’s lecture (in which he introduced combinators)with computer-aided explorations of the realm of combinators and withdocuments filling in gaps in the historical context. As a measure ofhow widely Sheffer’s and Schönfinkel’s reductions areknown, we appeal to the fact that the first is part of standard introcourses in logic, whereas the second is not. Undoubtedly, one of thereasons for this is that Schönfinkel’s process to eliminatebound variables is conceptually more opulent than defining a few truthfunctions from $\mid$ (or $\downarrow$). Another reason may bethat Schönfinkel, perhaps, did not place a sufficiently strongemphasis on the intermediate step that allows the elimination of allother logical connectives and quantifiers via “nextand.”The importance of this step was also overlooked in the introduction tothe English translation of Schönfinkel’s paper, which waswritten more than 30 years after the original publication. We may alsonote that although “nextand” is an operator in thestandard logical sense, it is binary—unlike $\forall$ and$\exists$, which are unary.

If $A\mid B \Leftrightarrow_\textrm{df} \lnot(A\land B)$ is added asa definition to SL, then the result is aconservativeextension, and it becomes provable that for any formula$A(p_0,\ldots,p_n)$ (i.e., for a formula containing the displayedpropositional variables and some connectives) there is a formula$B(p_0,\ldots,p_n)$ containing only the connective $\mid$, and$B(p_0,\ldots,p_n)\Leftrightarrow A(p_0,\ldots,p_n)$ itself isprovable. $\mid$ is, of course, interpreted as the“nand” truth function. “Nand” as a binaryconnective or as a binary truth function is of the same sort of objectas conjunction, disjunction, etc.

The first stage in Schönfinkel’s extension of FOL isanalogous. The addition of $\mid^-$ is (also) a conservativeextension of FOL, and every occurrence of $\mid^-$ can beeliminated. (We noted that $\mid^-$ is a binary operator, and so itmay be thought to combine a quantifier ($\exists$) with connectives($\lnot$, $\land$), but $\mid^-$ of course, does not introduceany objects that are not definable in FOL.)

The second stage in Schönfinkel’s extension of FOL isslightly different. $UXY$ is definable in FOL only for one-placepredicates $P$ and $Q$ (or for predicates of higher arity when thevariable in their last argument is bound). Thus, in general, neither$U$ nor the combinators are definable in FOL.

The elimination of bound variables goes beyond the resources of FOL.The combinators are not only undefinable, but they are new kinds ofobjects—which are absent from FOL itself. Also, the intermediatesteps of the bound variable elimination procedure presuppose thatfunctions of several arguments can be viewed as functions in onevariable, and the other way around.^[7] Enriching a presentation of FOL with predicate letters that havesufficiently many arguments in the right order would be more or lessunproblematic, and it would add objects to the language that wouldhave the same sort of interpretation as other predicates. A potentialproblem though is that for each predicate, infinitely many($\aleph_0$ many) new predicates would be needed—together withaxioms stipulating the intended equivalences between the meanings ofthe variants of the predicates. Notationally, these steps amount topadding predicate symbols with extra arguments, omitting somearguments, as well as permuting and regrouping the arguments. Althoughsome of these additions may look superfluous or too fussy, for theunderstanding of Schönfinkel’s procedure to eliminate boundvariables, it is crucial to note that formulas are viewed asstructured strings of symbols.^[8]

In conclusion to this section, it is important to emphasize that thereareno questions of consistency with respect to the abovereduction process, because it can be viewed—or described incontemporary terms—as awell-defined algorithm. It is acompletely different issue that if we consider the language of FOLexpanded with combinators, then the resulting system is inconsistent,because CL is powerful enough to define the fixed point of anyfunction. The effect of having fixed points for allfunctions—including truth functions—may be thought toamount to adding certain biconditionals (which may or may not bevalid) as axioms. (For instance, Russell’s paradox emerges fromthe fixed point of the negation connective.) Notably, both FOL and(pure) CL areconsistent.

1.3 Alternative approaches: basic logic and predicate functors

In this section we briefly outline two ideas that are related toSchönfinkel’s work or are motivated by his use ofcombinators in the elimination of bound variables.

Fitch’s metalogic
From the late 1930s, Frederic Fitch worked on a logic that he calledbasic logic. The label is motivated by his aim to provide aframework in which any logic could be formalized. Fitch’sapproach is utterlysyntactic (much likeSchönfinkel’s), and “formalization” is to beunderstood asencoding a formally described system inanother—not unlike the arithmetization of the syntax inGödel’s incompleteness theorem.

In 1942, Fitch introduced a logic that he labeled $K$. Theexpressions in $K$ are formed like combinatory terms by a binaryapplication operation, which is not assumed to be associative. (Seethe definition of combinatory terms in the next section.) However, theconstants of $K$ do not coincide with the constants of pure CL.Fitch uses10 constants: $\varepsilon$, $o$,$\acute{\varepsilon}$, $\acute{o}$, $W$, $=$, $\land$,$\lor$, $E$ and $*$. The first five constants are combinators,though the notation may suggest a different (informal) meaning.‘$=$’ is the syntactical identity of expressions.‘$\land$’ and ‘$\lor$’ are intended tostand for “and” and “or.” ‘$E$’is the analogue of Schönfinkel’s $U$, but it correspondsto a non-vacuous existential quantifier. Finally, ‘$*$’is similar to the transitive closure operator for binary relations orthe Kleene star. Notably, there is no negation or universal quantifierin the system. The uses of the constants are characterized asfollows—somewhat like axioms characterize combinators.

$=ab$ if and only if $a$ and $b$ are(syntactically) the same expression
$\varepsilon ab$ if and only if $ba$
$oabc$ if and only if $a(bc)$
$\acute{\varepsilon} abc$ if and only if $bac$
$\acute{o} abcd$ if and only if $a(bc)d$
$Wab$ if and only if $abb$
$\land ab$ if and only if $a$ and $b$
$\lor ab$ if and only if $a$ or $b$
$Eb$ if and only if $\exists a.\,ba$
$*abc$ if and only if $abc$ and $\existsd.\,abd\&adc$

In CL, the axioms are followed up with notions such as one-step andweak reduction, the latter of which can be viewed as a computation orinference step. (See the next section for some of these notions.)Similarly, an axiomatic calculus for FOL, for instance, would containrules of inference in addition to the axioms. One of the obstacles topenetrate the various presentations of basic logic is the lack of asimilar formulation.

During the next two decades or so after his first paper on basiclogic, Fitch published a series of papers on basic logic devoted to(1) therepresentation of recursive functions (i.e., ademonstration of the possibility of the arithmetization of syntax),(2) $K^\prime$, an extension of $K$ withnegation,universal quantifier and # (the dual of the $*$ operator),(3) theconsistency of $K$ and $K^\prime$, (4) $L$, anextension of $K^\prime$ withimplication andnecessityoperators, (5) thedefinability of some of the constants suchas $*$ and #, as well as $E$.

The combinators that are included in $K$ (hence, in all itsextensions) are $\textsf{T}$, $\textsf{B}$ and $\textsf{W}$.$\acute \varepsilon$ and $\acute o$ are the ternary version of$\textsf{T}$ and the quaternary version of $\textsf{B}$,respectively. Russell’s paradox involves negation, but (eithervariant of) Curry’s paradox is positive, in the sense that itrelies on one or two theorems of the positive implicational logic ofDavid Hilbert. This means that if the various systems of basic logic,especially $K^\prime$ and $L$ are consistent, then they eithercannot contain full abstraction, or the notions of implication,entailment and identity should differ from their usual counterparts.Indeed, $K$, $K^\prime$ and $L$ arenot extensionalsystems. That is, even if two expressions applied to the sameexpression are always equal, the equality of the applied expressionsdoes not follow. Turning basic logic into an extensional system provedless than straightforward. Fitch’s system $JE^\prime$ wasshown to be inconsistent by Myhill, which led to a more complicatedformulation of the conditions for extensional identity.

Basic logic has not (yet) become a widely used general framework forthe description of formal systems; however, renewed interest in thisapproach is signaled by Updike (2010), which attempts to situate basiclogic in the broader context of foundational work at the middle of the20th century.

Quine’s elimination strategy
From the late 1930s, W. V. O. Quine worked on an alternative way toeliminate bound variables from first-order logic. It is plausible toassume that Schönfinkel’s goal was to find a singleoperator in classical logic and then to eliminate the boundvariables—as he claims in Schönfinkel (1924)—ratherthan defining an overarching symbolic system to describe allmathematics. Nonetheless, CL was soon fused with classical logic in amore free-wheeling fashion, which resulted in an inconsistentsystem.

Quine saw the way out of a situation where inconsistency may arise viaimplicit typing of constants that are to some extent similar tocombinators. He called such constantspredicate functors, andintroduced several groups of them, the last one in Quine (1981).

The most common presentations of FOL stipulate that an $n$-placepredicate followed by asequence of $n$ terms (possibly,punctuated by commas and surrounded by parentheses) is a formula.(This is in contrast with Schönfinkel’s view of formulasand in accordance with the informal and formal interpretations ofpredicates as $n$-ary relations. In other words, FOL does not permit“currying” of predicates or of their interpretations.)Quine subscribes to the view that sequences of terms followpredicates.

Predicate functors are not applicable to each other—unlike thecombinators are. This is a point that Quine repeatedly emphasizes.Atomic predicates are the predicates of a first-order language,whereascomplex predicates are obtained by applying a predicatefunctor (of appropriate arity) to predicates (which may be atomic orcomplex).

The prohibition of self-application together with the use of“flat” sequences of arguments means thatinfinitelymany predicate functors are needed to ensure the elimination ofbound variables from all formulas of FOL. To explain the problemquickly: a permutation of a pair of elements that are arbitrarily farapart cannot be ensured otherwise. Just as combinators may be dividedinto groups based on their effect, Quine was able to select predicatefunctors that can be grouped together naturally based on theireffects. Indeed, the groups of predicate functors are similar toclasses of combinators, though Quine’s labels are often sublime.In order to give a concrete example of this alternative approach, weoutline a slightly modified version of a set of predicate functorsfrom Quine (1981).

A first-order language with $\mid^-$ as the only operator isassumed. ($F$ and $G$ are metavariables for predicates in thepredicate functor language.) $\wr^n$ $\textit{Inv}^n$,$\textit{inv}^n$, $\textit{Pad}^{n+1}$ and $\textit{Ref}^n$ arepredicate functors, for every $n\in\omega$. A formula of FOL isrewritten into a formula in a predicate functor language byapplications of the following clauses.

A variable $x$ and a predicate $P$ of FOL is $x$ and $P$,respectively, in the predicate functor language.
$Fx_1x_2\ldots x_n\mid^{x_1}Gx_1x_2\ldots x_n \mathbin{{:}{=}{:}}(F\wr G)x_2\ldots x_n$, where $x_2,\ldots, x_n$ are distinct from$x_1$, and $F$ and $G$ are followed by the same sequence ofvariables.
$Fx_1x_2\ldots x_n \mathbin{{:}{=}{:}} (\textit{Inv }F)x_2\ldotsx_nx_1$
$Fx_1x_2\ldots x_n \mathbin{{:}{=}{:}} (\textit{inv}F)x_2x_1\ldots x_n$
$Fx_2\ldots x_n \mathbin{{:}{=}{:}} (\textit{Pad } F)x_1x_2\ldotsx_n$
$Fx_1x_1x_2\ldots x_n \mathbin{{:}{=}{:}} (\textit{Ref }F)x_1x_2\ldots x_n$

There is an obvious similarity between $\textit{Ref}$ and$\textsf{W}$, $\textit{Pad}$ and $\textsf{K}$, as well as$\textit{Inv}$ and $\textit{inv}$ and various combinators withpermutative effects (e.g., $\textsf{C}$ and $\textsf{T}$). If$\mid^-$ is the only operator in the first-order language, then allformulas, which are not atomic, are almost of the form of theleft-hand side expression in 2. What has to be assured is that theside condition is satisfied, and that is where clauses 3–6enter. Although the various $n$-ary versions of $\wr$,$\textit{inv}$, $\textit{Pad}$ and $\textit{Ref}$ could beconflated (by ignoring unaffected arguments), $\textit{Inv}$ clearlystands for infinitely many predicate functors, because$x_1,\ldots,x_n$ cannot be ignored or omitted.

It may be interesting to note that there is a difference between$\wr$ and Schönfinkel’s $U$. Not only the place of thebound variable is different, but $\wr$ builds in contraction for$n-1$ variables (which are separated by $\mid^-$ and other symbolsin the left-hand expression).

Quine intended the predicate functor language to lead to a novelalgebraization of first-order logic. While bound variables can beeliminated using predicate functors, Quine never defined an algebra inthe usual sense—something similar, for instance, to polyadic orcylindric algebras. Predicate functors, by design, have a very limitedapplicability, which has the unfortunate side effect that they seem tobe of little interest and not much of use outside their intendedcontext.

2. Combinatory terms and their main properties

2.1 Reduction, equality and their formalizations

The paradoxes that were discovered by Georg Cantor and BertrandRussell in the late 19th–early 20th century both involveself-membership of a set. The ramified theory of types due to AlfredN. Whitehead and Bertrand Russell, andZF (the formalization of set theory named after Ernst Zermelo andAbraham A. Fraenkel) exclude self-membership. However, there seems tohave been always a desire to create a theory that allowsself-membership or self-application. Indeed, one of Curry’smotivations for the development of CL was the goal to construct aformal language that includes a wide range of well-formed expressions,some of which—under certain interpretations—may turn outto be meaningless. (This idea may be compared to thevon Neumann–Bernays–Gödel formalization of set theory, in which—without the axiom offoundation—the Russell class can be proved not to be a set,hence, to be a proper class.)

A few natural language examples provide a convenient illustration toclarify the difference between (1), that is a well-formed (butmeaningless) expression and (2), which is a meaningful (butill-formed) sentence. (The meaningfulness of (2), of course, should betaken with a grain of salt. In reality,Kurt Gödel proved the system of PM to be incomplete in 1930. Thus (2) may beguessed—using syntactic and semantics clues—to be adistorted version of (2′) Peano arithmetic was proved to beincomplete by Gödel in 1930.)

(1): The derivative of $\lambda x\,(x^2+4x-6)$ wishes to declarethat functions are smart.
(2): Peano arithmetics prove incomplete with Gödel at 1930.

After these informal motivations, we turn to CL proper and introducesome of its notions a bit more formally.

Theobjects in CL are calledterms.^[9] Terms may be thought to be interpreted as functions (as furtherexplained in section 4.1).Primitive terms comprisevariables andconstants, whereascompound termsare formed by combining terms. Usually, a denumerable set (i.e., a setwith cardinality $\aleph_0$) of variables is included, and theconstants include some (undefined)combinators. (We use$x,y,z,v,w,u,x_0,\ldots$ as variables in the object language, and$M,N,P,Q,\ldots$ as metavariables that range over terms.)

Terms are inductively defined as follows.

(t1): If $x$ is a variable, then $x$ is a term;
(t2): if $c$ is a constant, then $c$ is a term;
(t3): if $M$ and $N$ are terms, then ($MN$) is a term.

In the above definition, (t3) conceals the binary operation thatconjoins the two terms $M$ and $N$. This operation is calledapplication, and it is often denoted by juxtaposition, that is,by placing its two arguments next to each other as in ($MN$).

Application is not assumed to possess additional properties (such ascommutativity), because its intended interpretation isfunctionapplication. For instance, $((vw)u)$ and $(v(wu))$ aredistinct terms—just as the derivative of $\lambdax.\,x^2+4x-6$ applied to 8 (that is, ($\lambda x.\,2x+4)8=20$) isdifferent from the derivative of 90 (that is, $(8^2+32-6)'=0$).Using $\lambda$ notation, the two terms in the example may beexpressed as

\[ ((\lambda y.\,y')(\lambda x.\,x^2+4x-6))8\]

\[(\lambda y.\,y')((\lambda x.\,x^2+4x-6)8).\]

If terms are viewed as structured strings (where parentheses showgrouping), then the number of distinct terms associated to a string oflength $n$ is theCatalan number $C_{n-1}$. For anon-negative integer $n$ (i.e., for $n\in\mathbb{N}$),

\[C_n = \frac{1}{n+1} {2n \choose n}.\]

The first seven Catalan numbers are $C_0=1$, $C_1=1$, $C_2=2$,$C_3=5$, $C_4=14$, $C_5=42$ and $C_6=132$. As an illustration,we may take—for simplicity—strings consisting of $x$s,because the terms are to differ only in their grouping. Clearly, ifthe term is $x$ or $xx$, that is of length 1 or 2, then there isonly one way to form a term, that is, there exists just one possibleterm in each case. If we start with three $x$s, then we may form$(xx)x$ or $x(xx)$. If the length of the term is 4, then the fiveterms are: $xxxx$, $x(xx)x$, $xx(xx)$, $x(xxx)$ and $x(x(xx))$. (It is a useful exercise to try to list the 14 distinct termsthat can be formed from 5 $x$s.)

The usual notational convention in CL is todrop parenthesesfrom left-associated terms together with the outmost pair. Forinstance, $xyz$ would be fully written as $((xy)z)$, whereas$xy(xz)$ and $(xy)(xz)$ are both “shorthand versions”of the term $((xy)(xz))$ (unlike $xyxz$). Grouping in termsdelineates subterms. For instance, $xy$ is a subterm of each of theterms mentioned in this paragraph, whereas $yz$ and $yx$ aresubterms of none of those terms.

Subterms of a term are recursively defined as follows.

(s1): $M$ is a subterm of $M$;
(s2): if $M$ is a subterm of $N$ or of $P$, then $M$ is asubterm of $NP$.

Incidentally, the notion of free variables is straightforwardlydefinable now: $x$ is a free variable of $M$ iff $x$ is asubterm of $M$. The set of free variables of $M$ is sometimesdenoted by $\textrm{fv}(M)$.

All terms are interpreted as functions, and combinators are functionstoo. Similarly, to some numerical and geometrical functions, that canbe described and grasped easily, the combinators that are frequentlyencountered can be characterized as perspicuous transformations onterms. (Sans serif letters denote combinators and$\mathbin{\triangleright_1}$ denotesone-step reduction.)

Definition. (Axioms of some well-known combinators)

$\textsf{S}xyz \mathbin{\triangleright_1} xz(yz)$	$\textsf{K}xy \mathbin{\triangleright_1} x$	$\textsf{I}x \mathbin{\triangleright_1} x$
$\textsf{B}xyz \mathbin{\triangleright_1} x(yz)$	$\textsf{T}xy \mathbin{\triangleright_1} yx$	$\textsf{C}xyz \mathbin{\triangleright_1} xzy$
$\textsf{W}xy \mathbin{\triangleright_1} xyy$	$\textsf{M}x \mathbin{\triangleright_1} xx$	$\textsf{Y}x \mathbin{\triangleright_1}x(\textsf{Y}x)$
$\textsf{J}xyzv \mathbin{\triangleright_1} xy(xvz)$	$\textsf{B}^\prime xyz \mathbin{\triangleright_1} y(xz)$	$\textsf{V}xyz \mathbin{\triangleright_1} zxy$

These axioms tacitly specify thearity of a combinator as wellas theirreduction (orcontraction) pattern. Perhaps,the simplest combinator is theidentity combinator$\textsf{I}$, that applied to an argument $x$ returns the same$x$. $\textsf{K}$ applied to $x$ is a constant function, becausewhen it is further applied to $y$, it yields $x$ as a result, thatis, $\textsf{K}$ is a cancellator with respect to its secondargument. $\textsf{W}$ and $\textsf{M}$ areduplicators,because in the result of their application one of the arguments(always) appears twice.^[10] $\textsf{C}$, $\textsf{T}$ and $\textsf{V}$ arepermutators, because they change the order of some of theirarguments. $\textsf{B}$ is anassociator, because$\textsf{B}xyz$ turns into a term in which $y$ is applied to $z$before $x$ is applied to the result. $\textsf{Y}$ is thefixedpoint combinator, because for any function $x$, $\textsf{Y}x$is the fixed point of that function (see section 2.3). The combinator$\textsf{B}^\prime$ is an associator and a permutator, whereas$\textsf{S}$ and $\textsf{J}$ are also duplicators. $\textsf{S}$is very special and it is called thestrong compositioncombinator, because when applied to two functions, let us say, $g$and $f$ (in that order), as well as $x$, then the resulting term$gx(fx)$ expresses the composition of $g$ and $f$ both appliedto the same argument $x$.

These informal explications did not mention any restrictions on thesort of functions $x,y,z,f,g,\ldots$ may be. However, the axiomsabove limit the applicability of the combinators to variables.Intuitively, we would like to say that given any terms, that is, anyfunctions $M$ and $N$, $\textsf{W}MN$ one-step reduces to$MNN$ (possibly, as a subterm of another term). For example, $M$may be $\textsf{K}$ and $N$ may be $yy$, and then$\textsf{WK}(yy)\triangleright_1\textsf{K}(yy) (yy)$. The latterterm suggests a further one-step reduction, and indeed we might beinterested in successive one-step reductions—such as thoseleading from $\textsf{WK}(yy)$ to $yy$. A way to achieve thesegoals is to formalize (a theory of) CL starting with the standardinequational logic but to omit the anti-symmetry rule and toadd certain other axioms and rules.

Inequational Calculus for CL ($\text{CL}_\triangleright$).

$M\triangleright M$	$\textsf{S}MNP\triangleright MP(NP)$	$\quad\textsf{K}MN\triangleright M$
$\dfrac{M\triangleright N \quad N\trianglerightP}{M\triangleright P}$	$\dfrac{M\triangleright N}{MP\triangleright NP}$	$\dfrac{M\triangleright N}{PM\triangleright PN}$

The use of metavariables encompassessubstitution (that weillustrated above on the term $\textsf{W}MN)$. The identity axiomand the rule of transitivity imply that $\triangleright$ is atransitive and reflexive relation. The last two rules characterizeapplication as an operation that ismonotone in both of itsargument places. $\text{CL}_\triangleright$ includes only$\textsf{S}$ and $\textsf{K}$, because the other combinators aredefinable from them—as we already mentioned in section 1.2, andas we explain more precisely toward the end of this section.

The set of combinators $\{\textsf{S},\textsf{K}\}$ is called acombinatory base, that is, these two combinators are theundefined constants of $\text{CL}_\triangleright$. To give an ideaof aproof in this calculus, the following steps may be piecedtogether to prove $\textsf{SKK} (\textsf{KSK})\triangleright\textsf{S}$. $\textsf{KSK}\triangleright \textsf{S}$ is an instanceof an axiom. Then $\textsf{SKK}(\textsf{KSK})\triangleright\textsf{SKKS}$ is obtained by right monotonicity, andfurther, $\textsf{SKK}(\textsf{KSK})\triangleright\textsf{S}$results by instances of the $\textsf{S}$ and $\textsf{K}$ axiomstogether with applications of the transitivity rule.

The relation $\triangleright$ is calledweak reduction, andit may be defined alternatively as follows. (‘Weakreduction’ is a technical term used in CL to distinguish thisrelation on the set of terms from some other relations, one of whichis called ‘strong reduction’.) A term that is either ofthe form $\textsf{S}MNP$ or of the form $\textsf{K}MN$ is aredex, and the leading combinators ($\textsf{S}$ and$\textsf{K}$, respectively) are theheads of the redexes. Ifa term $Q$ contains a subterm of the form $\textsf{S}MNP$, then$Q^\prime$, which is obtained by replacing that subterm by$MP(NP)$ is aone-step reduct of $Q$. (Similarly, for theredex $\textsf{K} MN$ and $M$.) That is, $Q\trianglerightQ^\prime$ in both cases.Reduction then may be defined as thereflexive transitive closure of one-step reduction. This notion iscompletely captured by $\text{CL}_\triangleright$. Thecalculus $\text{CL}_\triangleright$ iscomplete in the sensethat if $M\triangleright N$ in the sense we have just described,then $\text{CL}_\triangleright$ proves $M\triangleright N$. (It iseasy to see that the converse implication is true too.)

The notion of reduction is a weaker relation than one-step reduction,and so it is useful to distinguish a subclass of terms using thestronger relation. A term is innormal form (nf) when itcontains no redexes. Note that one-step reduction does not need todecrease the total number of redexes that a term contains, hence, itdoes not follow that every term can be turned into a term in nf viafinitely many one-step reductions. Indeed, some terms do not reduce toa term in nf.

Reduction is arguably an important relation between terms that denotefunctions. The typical steps in a program execution and in otherconcrete calculations are function applications rather than moves inthe other direction, what is calledexpansion. However, thenotion of the equality of functions is familiar to everybody frommathematics, and the analogous notion has been introduced in CL too.The transitive, reflexive, symmetric closure of the one-step reductionrelation is called (weak)equality. A formalization ofequational CL may be obtained by extending the standard equationallogic with combinatory axioms and rules characterizing the combinatoryconstants and the application operation.

Equational Calculus for CL ($\text{CL}_=$).

$M=M$	$\textsf{K}MN=M$	$\quad\textsf{S}MNP=MP(NP)\quad$
$\quad\dfrac{M=N \quad N=P}{M=P}\quad$	$\dfrac{M=N}{N=M}$	$\dfrac{M=N}{MP=NP}$	$\dfrac{M=N}{PM=PN}$

The first axiom and the first two rules constitute equational logic.The constants are again the combinators $\textsf{S}$ and$\textsf{K}$. Note that $\text{CL}_=$ could have been defined asan extension of $\text{CL}_\triangleright$ by adding the rule ofsymmetry, that would have paralleled the description of the definitionof equality from reduction as its transitive, symmetric closure. Wechose instead to repeat the inequational axioms and rules with the newnotation (and add the rule of symmetry) to make the two definitionsself-contained and easy to grasp. The two characterizations of $=$coincide—as those of $\triangleright$ did.

$\text{CL}_\triangleright$ and $\text{CL}_=$ share a feature thatmay or may not be desirable—depending on what sort ofunderstanding of functions is to be captured. To illustrate the issue,let us consider the one-place combinators $\textsf{SKK}$ and$\textsf{SK}(\textsf{KK})$. It is easy to verify that$\textsf{SKK}M\triangleright M$ and $\textsf{SK}(\textsf{KK})M\triangleright M$. However, neither $\textsf{SKK}\triangleright\textsf{SK}(\textsf{KK})$ nor$\textsf{SK}(\textsf{KK})\triangleright \textsf{SKK}$ is provable in$\text{CL}_\triangleright$; a fortiori, the equality of the twoterms in not provable in $\text{CL}_=$. This means that$\text{CL}_\triangleright$ and $\text{CL}_=$ formalizeintensional notions of functions, where“intensionality” implies that functions that give the sameoutput on the same input may remain distinguishable.

The archetypical intensional functions that one is likely to encounterarealgorithms. As examples, we might think of variousspecifications to calculate the decimal expansion of $\pi$, orvarious computer programs that behave in the same way. For instance,compilers (for one and the same language) may differ from each otherby using or not using some optimizations, and thereby, producingprograms from a given piece of code that have identicalinput–output behavior but different run times.

If functions that are indistinguishable from the point of view oftheir input–output behavior are to be identified, that is, anextensional understanding of functions is sought, then$\text{CL}_\triangleright$ and $\text{CL}_=$ have to be extendedby the following rule, (where the symbol $\ddagger$ is to bereplaced by $\triangleright$ or $=$, respectively).

\[\frac{Mx\ddagger Nx}{M\ddagger N} \text{ where } x \text{ is not free in } MN.\]

2.2 Church–Rosser theorems and consistency theorems

The calculuses $\text{CL}_\triangleright$ and $\text{CL}_=$ of theprevious section formalize reduction and equality. However,$\triangleright$ and $=$ have some further properties that areimportant when the terms are thought to stand for functions. The nexttheorem is one of the earliest and best-known results about CL.

Church–Rosser theorem (I). If $M$ reduces to $N$ and$P$, then there is a term $Q$ to which both $N$ and $P$reduce.

Figure 1. Illustration for theChurch–Rosser theorem (I)

If we think that reduction is like computing the value of a function,then the Church–Rosser theorem—in a firstapproximation—can be thought to state that the final result of aseries of calculations with a term is unique—independently ofthe order of the steps. This is a slight overstatement though, becauseuniqueness implies that each series of calculations ends (or“loops” on a term). That is, if there is a unique finalterm, then only finitely many distinct consecutive calculation stepsare possible.

A coarse analogy with elementary arithmetic operations, perhaps, canshed some light on the situation. The addition and multiplication ofnatural numbers always yield a natural number. However, if division isincluded then it is no longer true that all numerical expressionsevaluate to a natural number, since $7/5$ is a rational number thatis not a natural one, and $n/0$ is undefined (even if $n$ werereal). That is, some numerical expressions do not evaluate to a(natural) number. Although the analogy with combinatory terms is notvery tight, it is useful. For instance, $n/0$ (assuming that thecodomain of the function $\lambda n.\,n/0$ is extended to permit$r$ to be rational) could be implemented on a computer by a loop(that would never terminate when executed if $n\ne0$) which would gothrough an enumeration of the rational numbers trying to find an $r$such that $r\cdot0=n$.

The combinatory terms $\textsf{WWW}$ and$\textsf{WI}(\textsf{WI})$ are, perhaps, the simplest examples ofterms that do not have a normal form. Both terms induce an infinitereduction sequence, that is, an infinite chain of successiveone-step reductions. To make the example more transparent, let usassume for a moment that $\textsf{W}$, $\textsf{I}$,$\textsf{C}$, etc. are not defined from $\textsf{K}$ and$\textsf{S}$, but are primitive constants. The contraction of theonly redex in $\textsf{WWW}$ returns the same term, which shows thatuniqueness does not imply that the term is in nf. The contraction ofthe only redex in $\textsf{WI}(\textsf{WI})$ gives$\textsf{I}(\textsf{WI})(\textsf{WI})$ that further reduces to theterm we started with. A slightly more complicated example of a termthat has only infinite reduction sequences is$\textsf{Y}(\textsf{CKI})$. This term has a reduction sequence (inwhich each contracted redex is headed by $\textsf{Y}$) that containsinfinitely many distinct terms. It is also possible to create infinitereduction sequences that start with $\textsf{Y} (\textsf{CKI})$ andhave various loops too. To sum up, the Church–Rosser theorem, ingeneral, does not guarantee the uniqueness of the term $Q$. However,if $M$ hasa normal form then that isunique.

The Church–Rosser theorem is often stated as follows.

Church–Rosser theorem (II). If $N$ and $P$ are equal,then there is a term $Q$ to which both $N$ and $P$ reduces.

Figure 2. Illustration for theChurch–Rosser theorem (II)

The second form of the Church–Rosser theorem differs from thefirst in itsassumption. From the definition of equality as asuperset of reduction, it is obvious that the first form of thetheorem is implied by the second. However, despite the weakerassumption in the second formulation of the Church–Rossertheorem, the two theorems areequivalent. Equality is thetransitive, symmetric closure of reduction, which means that if twoterms are equal then there is a finite path comprising reduction andexpansion steps (which decompose into one-step reductions and one-stepexpansions, respectively). Then by finitely many applications of thefirst Church–Rosser theorem (i.e., by induction on the length ofthe path connecting $N$ and $P$), the first Church–Rossertheorem implies the second formulation.

Modern proofs of the Church–Rosser theorem for CL proceedindirectly because one-step reduction fails to have the diamondproperty. A binary relation $R$ (e.g., reduction) is said to havethediamond property when $xRy$ and $xRz$ imply that$yRv$ and $zRv$ for some $v$. If a binary relation $R$ has thediamond property, so does its transitive closure. To exploit thisinsight in the proof of the Church–Rosser theorem, a suitablesubrelation of reduction has to be found. The sought aftersubrelation should possess the diamond property, and its reflexivetransitive closure should coincide with reduction.

The following counterexample illustrates that one-step reductions of aterm may yield terms that further do not reduce to a common term inone step.$\textsf{SKK}(\textsf{KKS})\triangleright_1\textsf{SKKK}$ and$\textsf{SKK}(\textsf{KKS})\triangleright_1\textsf{K}(\textsf{KKS})(\textsf{K}(\textsf{KKS}))$, and then some of the potential reductionsequences are as follows.

$\textsf{SKKK}\triangleright_1\textsf{KK}(\textsf{KK})\triangleright_1\textsf{K}$
$\textsf{K}(\textsf{KKS})(\textsf{K}(\textsf{KKS}))\triangleright_1\textsf{KKS}\triangleright_1\textsf{K}$
$\textsf{K}(\textsf{KKS})(\textsf{K}(\textsf{KKS}))\triangleright_1\textsf{KK}(\textsf{K}(\textsf{KKS}))\triangleright_1\textsf{KK}(\textsf{KK})\triangleright_1\textsf{K}$
$\textsf{K}(\textsf{KKS})(\textsf{K}(\textsf{KKS}))\triangleright_1\textsf{K}(\textsf{KKS})(\textsf{KK})\triangleright_1\textsf{KKS}\triangleright_1\textsf{K}$
$\textsf{K}(\textsf{KKS})(\textsf{K}(\textsf{KKS}))\triangleright_1\textsf{K}(\textsf{KKS})(\textsf{KK})\triangleright_1\textsf{KK}(\textsf{KK})\triangleright_1\textsf{K}$

The failure of the diamond property is obvious once we note that$\textsf{SKKK}\triangleright_1\textsf{KK}(\textsf{KK})$ (only), but$\textsf{K}(\textsf{KKS})(\textsf{K}(\textsf{KKS}))$ does not reducein one step to $\textsf{KK}(\textsf{KK})$.

An appropriate subrelation of reduction is thesimultaneousreduction of a set of nonoverlapping redexes, which is denoted by$\triangleright _\textrm{sr}$. ‘Nonoverlapping’ meansthat there are no shared subterm occurrences between two redexes.$\triangleright_\textrm{sr}$ includes $\triangleright_1$ because aone-step reduction of a redex may be viewed instead as$\triangleright_\textrm{sr}$ of a singleton set of redexes.$\triangleright_\textrm{sr}$ is, obviously, included in$\triangleright$ (i.e., in reduction). These two facts imply thatthe reflexive transitive closure of $\triangleright_\textrm{sr}$ isreduction—when the tonicity of the reflexive transitive closureoperation (denoted by $^*$) is taken into account.

(1)–(3) summarize the key inclusions between the relationsmentioned.

(1): $\triangleright_1\subseteq\triangleright_\textrm{sr}\;\Rightarrow\;\triangleright_1^*\subseteq\triangleright_\textrm{sr}^*$
(2): $\triangleright_\textrm{sr}\subseteq\triangleright\;\Rightarrow\;\triangleright_\textrm{sr}^*\subseteq\triangleright^*$
(3): $\triangleright_1^*\subseteq\triangleright^*\quad \textrm{ and}\quad\triangleright^*=\triangleright$.

The central property of $\triangleright_\textrm{sr}$ that we need isthe content of the following theorem.

Theorem. (Diamond property for $\triangleright_\textrm{sr}$)If $M\triangleright_\textrm{sr}N$ and$M\triangleright_\textrm{sr}P$ then there is a term $Q$ such thatboth $N\triangleright_\textrm{sr}Q$ and$P\triangleright_\textrm{sr}Q$.

The proof of this theorem is an easy induction on the term $M$. Theproperties of $\triangleright_\textrm{sr}$ guarantee that one ormore one-step reductions can be performed at once, but the reductionscannot interfere (or overlap) with each other.

Theconsistency of CL follows from the Church–Rossertheorem together with the existence of (at least two) distinct normalforms.

Theorem. (Consistency) CL is consistent, that is, there areterms that do not reduce to each other, hence they are not equal.

Not all terms have an nf, however, many do. Examples, first of all,include $\textsf{S}$ and $\textsf{K}$. (The variables, ifincluded, of which there are $\aleph_0$ many, are all in nf.) Noneof these terms contains a redex, hence each reduces only to itself. Bythe Church–Rosser theorem, it is excluded that some term $M$could reduce to both $x$ and $\textsf{S}$ (making $\textsf{S}$equal to $x$).

The interaction between infinite reduction sequences and nfs deservesa more careful inspection though. The terms $\textsf{WWW}$,$\textsf{Y} (\textsf{CKI})$ and $\textsf{WI}(\textsf{WI})$ haveonly infinite reduction sequences. However, the existence of aninfinite reduction sequence for a term does not imply that the termhas no normal form (when the combinatory base is complete or containsa cancellator). $\textsf{Y} (\textsf{KI})$ reduces to$\textsf{KI}(\textsf{Y}(\textsf{KI}))$,$\textsf{KI}(\textsf{KI}(\textsf{Y}(\textsf{KI})))$, $\textsf{KI}(\textsf{KI}(\textsf{KI}(\textsf{Y}(\textsf{KI})))),\ldots$ as wellas to $\textsf{I}$.

A termweakly normalizes when it has an nf, whereas a termstrongly normalizes when all its reduction sequences lead to annf (hence, tothe nf) of the term. A computational analogue ofa strongly normalizing term is a (nondeterministic) program thatterminates on every branch of computation, whereas termination on atleast one branch is akin to weak normalization.

The importance of normalization led to a whole range of questions (andan extensive literature of answers). How does the order of thereduction steps (i.e., a reduction strategy) affect finding the nf (ifthere is one)? Are there combinatory bases that guarantee theexistence of normal forms for every combinator over that base? Toquickly illustrate possible answers to our sample questions, we startwith noting that if there is no combinator with a duplicative effectin a base, then all combinators over that base strongly normalize.This is a very easy answer, and as a concrete base, we could have, forexample, $\{\textsf{B},\textsf{C},\textsf{K}\}$ or $\{\textsf{B},\textsf{C},\textsf{I}\}$, which have some independent interest inview of their connection to simply typed calculuses. However, thesebases are far from being combinatorially complete and even a fixedpoint combinator is undefinable in them.

We could ask a slightly different question: If we start with the base$\{\textsf{S},\textsf{K}\}$ and we omit $\textsf{S}$, then we getthe base $\{\textsf{K}\}$ and all the combinators stronglynormalize, but what if we omit $\textsf{K}$? Do the combinators over$\{\textsf{S}\}$ strongly normalize or at least normalize? Theanswer is “no.” A term (discovered by Henk Barendregt inthe early 1970s) that shows the lack of strong normalization is$\textsf{SSS}(\textsf{SSS})(\textsf{SSS})$. The first $\textsf{S}$is the head of a (indeed,the only) redex, and the headreduction sequence of this term is infinite. Since $\{\textsf{S}\}$does not contain any combinator with a cancellative effect, theexistence of an infinite reduction sequence for a term means that theterm has no nf. There are shorter combinators over the base$\{\textsf{S}\}$ without an nf, for example,$\textsf{S}(\textsf{SS})\textsf{SSSSS}$ comprises only eightoccurrences of $\textsf{S}$.

The sorts of questions we illustrated here (or rather, the answers tothem) can become a bit technical, because they often involve conceptsand techniques from graph theory, automata theory and the theory ofterm-rewriting.

2.3 The existence of fixed points and combinatorial completeness

Schönfinkel proved that $\textsf{S}$ and $\textsf{K}$ sufficeto define the other combinators he introduced, and we mentioned in thedefinition of $\text{CL}_\triangleright$ that the set of constantsis limited to $\textsf{S}$ and $\textsf{K}$, because othercombinators could be defined from those.

To demonstrate the sense in which definability is understood here weconsider the example of $\textsf{B}$. The axiom for $\textsf{B}$is $\textsf{B} xyz\triangleright_1x(yz)$, and if we take$\textsf{S}(\textsf{KS}) \textsf{K}$ instead of $\textsf{B}$, thenthe following reduction sequence results.

\[\textsf{S}(\textsf{KS})\textsf{K}xyz\triangleright_1\textsf{KS}x(\textsf{K}x)yz\triangleright_1\textsf{S}(\textsf{K}x)yz\triangleright_1\textsf{K}xz(yz)\triangleright_1x(yz)\]

The term $\textsf{S}(\textsf{KS})\textsf{K}$ is in nf, however, tobe in nf is not a requirement for definability. It is more convenientto work with defining terms that are in nf, because an application ofa combinator that is not in nf could be started with reducing thecombinator to its normal form. (Also, there are always infinitely manycombinators that reduce to a combinator.) However, note that thepreference for choosing combinators in nf is not meant to imply that acombinator cannot be defined by two or more terms in nf; below we givetwo definitions (involving only $\textsf{S}$ and $\textsf{K}$) for$\textsf{I}$.

If the constants are $\textsf{S}$ and $\textsf{K}$, then thecombinators are all those terms that are formed from$\textsf{S}$ and $\textsf{K}$ (without variables). Once we havedefined $\textsf{B}$ as $\textsf{S}(\textsf{KS})\textsf{K}$, wemay use $\textsf{B}$ in further definitions as an abbreviation, andwe do that primarily to reduce the size of the resulting terms as wellas to preserve the transparency of the definitions.

The following list gives definitions for the other well-knowncombinators that we mentioned earlier. (Here ‘$=$’ isplaced between a definiendum and a definiens.)

$\textsf{I}=\textsf{SK}(\textsf{KK})$	$\textsf{T}=\textsf{B}(\textsf{SI})\textsf{K}$	$\textsf{C}=\textsf{B}(\textsf{T}(\textsf{BBT}))(\textsf{BBT})$
$\textsf{W}=\textsf{CSI}$	$\textsf{M}=\textsf{SII}$	$\textsf{Y}=\textsf{BW}(\textsf{BB}^\prime\textsf{M})(\textsf{BW}(\textsf{BB}^\prime\textsf{M}))$
$\textsf{V}=\textsf{BCT}$	$\textsf{B}^\prime=\textsf{CB}$	$\textsf{J}=\textsf{W}(\textsf{BC}(\textsf{B}(\textsf{B}(\textsf{BC}))(\textsf{B}(\textsf{BB})(\textsf{BB}))))$

The definitions are easily seen to imply that all these combinatorsdepend on both $\textsf{S}$ and $\textsf{K}$, but it is notobvious from the definitions that the defined combinators are mutuallyindependent, that is, that none of the listed combinators is definablefrom another one. (Clearly, some subsets suffice to define some of thecombinators.) We do not intend to give an exhaustive list ofinterdefinability between various subsets of these combinators, but tohint at the multiplicity and intricacy of such definitions, we list ahandful of them. We also introduce two further combinators$\textsf{S}^\prime$ and $\textsf{R}$.

$\textsf{I}=\textsf{SKK}$	$\textsf{I}=\textsf{WK}$	$\textsf{I}=\textsf{CK}(\textsf{KK})$
$\textsf{B}=\textsf{CB}^\prime$	$\textsf{S}^\prime=\textsf{CS}$	$\textsf{S}=\textsf{CS}^\prime$
$\textsf{W}=\textsf{S}^\prime\textsf{I}$	$\textsf{W}=\textsf{B}(\textsf{T}(\textsf{BM}(\textsf{BBT})))(\textsf{BBT})$	$\textsf{W}=\textsf{C}(\textsf{S}(\textsf{CC})(\textsf{CC}))$
$\textsf{R}=\textsf{BBT}$	$\textsf{Y}=\textsf{BM}(\textsf{CBM})$	$\textsf{Y}=\textsf{B}^\prime(\textsf{B}^\prime\textsf{M})\textsf{M}$

If the fixed point combinator $\textsf{Y}$ is not taken to be aprimitive, then there are various ways to define it—so far, wehave listed three.

Fixed point theorem. For any function $M$, there is a term$N$ such that $MN = N$.

The proof of this theorem is easy using a fixed point combinator,because a term that can play the rôle of $N$ is$\textsf{Y}M$.

Some of the definitions of $\textsf{Y}$ have slightly differentproperties with respect to reduction. But the importance of the fixedpoint combinator is that it ensures that all functions have a fixedpoint and allrecursive equations can be solved.

Both Haskell B. Curry and Alan Turing defined fixed point combinators(in CL or in the $\lambda$-calculus). If we consider thedefinitions

\[\textsf{Y}_1=\textsf{BM}(\textsf{BWB})\quad\textsf{Y}_2=\textsf{W}(\textsf{B}(\textsf{BW}(\textsf{BT})))(\textsf{W}(\textsf{B}(\textsf{BW}(\textsf{BT}))))\]

(where the subscripts are added to distinguish the two definitions),then we can see that $\textsf{Y}_1 M=M(\textsf{Y}_1M)$, but for$\textsf{Y}_2$, $\textsf{Y}_2M\triangleright M(\textsf{Y}_2M)$holds too. In this respect, $\textsf{Y}_1$ is similar toCurry’s fixed point combinator (and really, to any fixed pointcombinator), whereas $\textsf{Y}_2$ is like Turing’s fixedpoint combinator.

The fixed point theorem demonstrates—to some extent—theexpressive power of CL. However, fixed point combinators may bedefined from bases without a cancellator (as $\textsf{Y}_1$ and$\textsf{Y}_2$ show). The full power of CL (with the base$\{\textsf{S},\textsf{K}\}$) is enunciated by the followingtheorem.

Theorem. (Combinatorial completeness) If $f(x_1,\ldots,x_n)=M$ (where $M$ is a term containing no other variables than thoseexplicitly listed), then there is a combinator $\textsf{X}$ suchthat $\textsf{X} x_1\ldots x_n$ reduces to $M.$

The theorem’s assumption may be strengthened to exclude thepossibility that some occurrences of $x$ do not occur in $M$. Thenthe consequent may be strengthened by adding the qualification that$\textsf{X}$ is a relevant combinator, more specifically,$\textsf{X}$ is a combinator over $\{\textsf{B},\textsf{W},\textsf{C},\textsf{I}\}$ (a base that does not contain a combinatorwith cancellative effect), or equivalently, $\textsf{X}$ is acombinator over $\{\textsf{I},\textsf{J}\}$. (These bases correspondto Church’s preferred $\lambda\textsf{I}$-calculus.)

Combinatorial completeness is usually proved via defining a“pseudo” $\lambda$-abstraction (orbracket abstraction) in CL. There are various algorithms todefine a bracket abstraction operator in CL, that behaves as the$\lambda$ operator does in a $\lambda$-calculus. This operator isusually denoted by $[\,]$ or by $\lambda^*$. The algorithms differfrom each other in various aspects: (i) the set of combinators theypresuppose, (ii) the length of the resulting terms, (iii) whether theycompose into (syntactic) identity with the algorithm that translates acombinatory term into a $\lambda$-term, and (iv) whether theycommute with either of the reductions or equalities.

The first algorithm, the elements of which may already be found inSchönfinkel (1924), consists of the following clauses that areapplied in the order of their listing.

\[\begin{align}\tag{k} &[x].\,M=\textsf{K}M, \text{ where } x\notin\textrm{fv}(M) \\\tag{i} &[x].\,x=\textsf{I} \\\tag{$\eta$} &[x].\,Mx=M, \text{ where } x\notin\textrm{fv}(M) \\\tag{b} &[x].\,MN=\textsf{B}M([x].\,N), \text{ where } x\notin\textrm{fv}(M) \\\tag{c} &[x].\,MN=\textsf{C}([x].\,M)N, \text{ where } x\notin\textrm{fv}(N) \\\tag{s} &[x].\,MN=\textsf{S}([x].\,M)([x].\,N)\end{align}\]

For example, if this algorithm is applied to the term $\lambdaxyz.x(yz)$ (that is, to the $\lambda$-translation of$\textsf{B}$), then the resulting term is $\textsf{B}$. However,if $\eta$ is omitted then a much longer term results, namely,$\textsf{C}(\textsf{BB}(\textsf{BBI}))(\textsf{C}(\textsf{BBI})\textsf{I})$. Another algorithm, for example, consistsof clauses (i), (k) and (s).

3. Nonclassical logics and typed CL

3.1 Simple types

Combinatory terms are thought of as functions, and functions arethought to have adomain (a set of possible inputs) and acodomain (a set of possible outputs). For example, if a unaryfunction is considered as a set of ordered pairs, then the domain andcodomain are given by the first and second projections, respectively.If partial and non-onto functions are permitted, thensupersetsof the sets resulting from the first and second projections can alsobe domains and codomains.Category theory, where functions are components of categories (without a set theoreticreduction assumed), retains the notions of a domain and a codomain;moreover, every function has a unique domain and codomain.

Functions that have the same domain and codomain may be quitedifferent, however, by abstraction, they are of the same sort or type.As a simple illustration, let $f_1$ and $f_2$ be two functionsdefined as $f_1= \lambda x.\,8\cdot x$ and $f_2=\lambda x.\,x/3$.If $x$ is a variable ranging over reals, then $f_1$ and $f_2$have the same domain and codomain (i.e., they have the same type$\mathbb{R}\rightarrow\mathbb{R}$), although $f_1\ne f_2$, because$f_1(x)\ne f_2(x)$ whenever $x\ne0$. The usual notation toindicate that a function $f$ has $A$ as its domain and $B$ asits codomain is $f\colon A\rightarrow B$. It is a happy coincidencethat nowadays ‘$\rightarrow$’ is often used in logics asa symbol for entailment or (nonclassical) implication.

Given a set of basic types (that we denote by $P$),types aredefined as follows.

If $p\in P$ then $p$ is a type;
if $A,B$ are types then $(A\rightarrow B)$ is a type.

To distinguish these types from other types—some of which areintroduced in the next section—they are calledsimpletypes.

The connection between combinators and types may be explained on theexample of the identity combinator. Compound combinatory terms areformed by the application operation. Premises of modus ponens can bejoined by fusion (denoted by $\circ$), which is like the applicationoperation in the strongest relevance logic $B$. $\textsf{I}x\triangleright x$ and so if $x$'s type is $A$, then$\textsf{I}x$'s type should imply $A$. Furthermore,$\textsf{I}x$'s type should be of the form $X\circ A$, for sometype $X$; then $\textsf{I}$ can be of type $A\rightarrow A$. Inthe example, we fixed $x$'s type, however, $\textsf{I}$ can beapplied to any term, hence, it is more accurate to say that$A\rightarrow A$ is the typeschema of $\textsf{I}$, orthat $\textsf{I}$'s type can be any formula of the form ofself-implication.

The type-assignment system TA$_\textrm{CL}$ is formally defined asthe following deduction system. (When implicational formulas areconsidered as types, the usual convention is to omit parentheses byassociation to the right.)

\[\Delta\vdash\textsf{S}\colon(A\rightarrow B\rightarrow C)\rightarrow (A\rightarrow B)\rightarrow A\rightarrow C\] \[\Delta\vdash\textsf{K}\colon A \rightarrow B\rightarrow A\] \[\frac{\Delta\vdash M\colon A\rightarrow B \quad\Theta\vdash N\colon A} {\Delta,\Theta\vdash MN\colon B}\]

Expressions of the form $M\colon A$ above are calledtypeassignments. A characteristic feature of type-assignment systemsis that if $M\colon A$ is provable then $A$ is considered to beone of the types that can be assigned to $M$. However, a provableassignment does not preclude other types from becoming associated tothe same term $M$, that is a type assignment does not fix the typeof a term rigidly. $\Delta$ and $\Theta$ on the left-hand side of$\vdash$ are sets of type assignments to variables, and they areassumed to be consistent—meaning that no variable may beassigned two or more types.

Type assignment systems are often calledCurry-style typingsystems. Another way to type terms is by fixing a type for eachterm, in which case each term has exactly one type. Such calculusesare calledChurch-style typing systems. Then, for example, theidentity combinator $\textsf{I}$ of type

\[(A\rightarrow A\rightarrow A)\rightarrow A\rightarrow A\rightarrow A\]

is not the same as the identity combinator $\textsf{I}$ of type

\[((B \rightarrow B)\rightarrow B)\rightarrow(B\rightarrow B)\rightarrow B.\]

The two styles of typing have quite a lot in common, but there arecertain differences between them. In particular, no self-applicationis typable in a Church-style typing system, whereas some of thoseterms can be assigned a type in a Curry-style typing system.Curry-style typing systems proved very useful in establishing variousproperties of CL and $\lambda$-calculuses. The Church-style typing,on the other hand, emulates more closely the typing in certainfunctional programming languages (without objects).

There is no one-one correspondence between types and combinators ineither style of typing: not all combinators can be assigned a type,and some implicational formulas cannot be assigned to any combinatoryterm. A combinator that can be assigned a type is said to betypable, and a type that can be assigned to a combinator issaid to beinhabited. For instance, $\textsf{M}$ has no(simple) type, because an implicational formula is never identical toits own antecedent. On the other hand, Peirce’s law,$((A\rightarrow B)\rightarrow A) \rightarrow A$ is not the type ofany combinator in the type assignment system TA$_\textrm{CL}$.Despite (or, indeed, due to) the discrepancy between implicationalformulas and combinatory terms, classes of implicational formulas thatcan be assigned to certain sets of combinatory terms coincide withsets of theorems of some important logics.

Theorem. $A\rightarrow B$ is a theorem of the intuitionisticimplicational logic, denoted by $IPC_\rightarrow$ or$J_\rightarrow$, iff for some $M$, $M\colon A\rightarrow B$ is aprovable type assignment in TA$_\textrm{CL}$, where the term $M$is built from $\textsf{S}$ and $\textsf{K}$, that is, $M$ is acombinator over the base $\{\textsf{S},\textsf{K}\}$.

A combinator that inhabits an implicational theorem encodes aproof of that theorem in the deduction systemTA$_\textrm{CL}$. There is an algorithm to recover the formulas thatconstitute a proof of the type of the combinator, moreover, thealgorithm produces a proof that is minimal and well-structured. Thecorrespondence between implicational theorems of intuitionistic logic(and their proofs) and typable closed $\lambda$-terms (orcombinators) is called theCurry–Howard isomorphism. Theusual notion of a proof in a Hilbert-style axiomatic system is quitelax, but it can be tidied up to obtain the notion oftraversingproofs. In a traversing proof there is a one-one correspondencebetween subterms of a combinator and the formulas in the traversingproof as well as between applications and detachments therein (cf.Bimbó 2007).

The above correspondence can be modified for other implicationallogics and combinatory bases. The next theorem lists correspondencesthat obtain between the implicational fragments of the relevancelogics $R$ and $T$ and some combinatory bases that are of interestin themselves.

Theorem. $A\rightarrow B$ is a theorem of $R_{\rightarrow}$(or $T_{\rightarrow}$) iff for some $M$, $M\colon A\rightarrowB$ is a provable type assignment where $M$ is a combinator over$\{\textsf{B}, \textsf{I},\textsf{W},\textsf{C}\}$ (or over$\{\textsf{B},\textsf{B}^\prime,\textsf{I},\textsf{S},\textsf{S}^\prime\}$).

The calculus $\textrm{TA}_\textrm{CL}$ may be amended by addingaxiom schemas for the combinators in the two bases. (The axiom schemasof the combinators that are not in these bases may be omitted from thecalculus or simply may be neglected in proofs.) Thenew axiomsare as follows.

\[\begin{align*}\textsf{B} &\colon (A\rightarrow B)\rightarrow(C\rightarrow A)\rightarrow C\rightarrow B \\\textsf{B}^\prime &\colon (A\rightarrow B)\rightarrow(B\rightarrow C)\rightarrow A\rightarrow C \\\textsf{C} &\colon (A\rightarrow B\rightarrow C)\rightarrow B\rightarrow A\rightarrow C \\\textsf{W} &\colon (A\rightarrow A\rightarrow B)\rightarrow A\rightarrow B \\\textsf{S}^\prime &\colon (A\rightarrow B)\rightarrow(A\rightarrow B\rightarrow C)\rightarrow A\rightarrow C \\\textsf{I} &\colon A\rightarrow A\end{align*}\]

The combinatory base$\{\textsf{B},\textsf{C},\textsf{W},\textsf{I}\}$ is especiallyinteresting, because these combinators suffice for a definition of abracket abstraction that is equivalent to the $\lambda$-abstractionof the $\lambda\textsf{I}$-calculus. To put it differently, allfunctions that depend on all of their arguments can be defined by thisbase. The other base allows the definition of functions that can bedescribed by terms in the class of the so-called hereditary rightmaximal terms (cf. Bimbó 2005). Informally, the idea behindthese terms is that functions can be enumerated, and then theirsuccessive applications should form a sequence in which the indexesare “globally increasing.”

A type assignment has two parts: aterm and aformula.The questions whether some term can be assigned a type and whethersome type can be assigned to a term are the problems oftypability and ofinhabitation, respectively. Althoughthese questions may be posed about one and the same set of typeassignments, the computational properties of these problems may differwidely.

Theorem. It is decidable if a term $M$ can be assigned atype, that is, if $M$ is typable.

The theorem is stated in a rather general way without specifyingexactly which combinatory base or which modification ofTA$_\textrm{CL}$ is assumed, because the theorem holds for anycombinatory base. Indeed, there is an algorithm that given acombinator decides if the combinator is typable, and for a typablecombinator produces a type too. Of course, in the combinatoriallycomplete base $\{\textsf{S},\textsf{K}\}$ all the combinators areexpressible as terms consisting of these two combinators only.However, this assumption is not needed for a solution of typability,though it might provide an explanation for the existence of a generalalgorithm.

Theproblem of inhabitation does not have a similar generalsolution, because the problem of the equality of combinatory terms isundecidable. Given a set of axiom schemas that are types ofcombinators with detachment as the rule of inference, the problem ofthedecidability of a logic can be viewed as the problem ofinhabitation. Indeed, if $A$ is an implicational formula, then todecide whether $A$ is a theorem amounts to determining if there is aterm (over the base that corresponds to the axiom schemas) that can beassigned $A$ as its type. (Of course, a more sophisticated algorithmmay actually produce such a term, in which case it is easy to verifythe correctness of the claim by reconstructing the proof of thetheorem.)

To see from where complications can emerge in the case ofdecidability, we compare the rule of theformation of terms andthe rule ofdetachment. Given a combinatory base and adenumerable set of variables, it is decidable by inspection whether atermis oris not in the set of the generated terms.That is, all the inputs of the rule are retained in the output assubterms of the resulting term. In contrast, an application ofdetachment results in a formula that is a proper subformula of themajor premise (and in the exceptional case when the major premise isan instance of self-identity it is identical to the minor premise).The lack of the retention of all subformulas of premises throughapplications of modus ponens is the culprit behind the difficulty ofsome of the decision problems of implicational logics. It is thensomewhat unsurprising that for many decidable logics there is adecision procedure utilizing sequent calculuses in which the cuttheorem and the subformula property hold. A solution to the problem ofinhabitation may run into difficulties similar to those that arise indecidability problems in general.

For example, the combinator $\textsf{K}$ can be assigned thefollowing type.

\[p\rightarrow(q\rightarrow(q\rightarrow q\rightarrow q)\rightarrow(q\rightarrow q)\rightarrow q\rightarrow q)\rightarrow p\]

$\textsf{SKK}$ can be assigned the type $p\rightarrow p$. There isa proof in TA$_\textrm{CL}$ ending in $\textsf{SKK}\colonp\rightarrow p$ that does not contain the long formula above.However, there is a proof of $\textsf{SKK}\colon p\rightarrow p$that contains the above formula the second antecedent of which is nota subformula of $p\rightarrow p$, indeed, the sets of thesubformulas of the two formulas are disjoint. (We picked two differentpropositional variables, $p$ and $q$ to emphasize this point.)Some important cases of the problem of inhabitation, however, aredecidable.

Theorem. It is decidable if a type has an inhabitant over thebase $\{\textsf{S},\textsf{K}\}$.

This theorem amounts to the typed version of the decidability of theimplicational fragment ofintuitionistic logic that is part ofGentzen’s decidability result (dating from 1935).

Theorem. It is decidable if a type has an inhabitant over thebase $\{\textsf{I},\textsf{C},\textsf{B}^\prime,\textsf{W}\}$.

The theorem is the typed equivalent of the decidability of theimplicational fragment of the logic ofrelevant implication.The decidability of $R_{\rightarrow}$ was proved by Saul A. Kripkein 1959 together with the decidability of the closely related$E_{\rightarrow}$ (the implicational fragment of thelogic ofentailment).

Theorem. It is decidable if a type has an inhabitant over thebase $\{\textsf{B},\textsf{B}^\prime,\textsf{I},\textsf{W}\}$.

the theorem is the typed version of the decidability of theimplicational fragment of the logic of ticket entailment$T_\rightarrow$, that was proved—together with thedecidability of $R_\rightarrow$ ($R_\rightarrow$ with the truthconstant $t$) and $T_\rightarrow^\textbf{t}$ ($T_\rightarrow$with the truth constant $t$)—in Bimbó and Dunn (2012)and Bimbó and Dunn (2013). An independent result (for$T_\rightarrow$ only) is in Padovani (2013), which extends Broda etal. (2004).

The decision procedures for $T_\rightarrow^\textbf{t}$ and$R_\rightarrow^\textbf{t}$ do not use $\textrm{TA}_\textrm{CL}$ oraxiomatic calculuses, instead, they build uponconsecutioncalculuses (i.e., sequent calculuses in which the structuralconnective is not assumed to be associative). The idea that there isan affinity between structural rules and combinators goes back atleast to Curry (1963). To tighten the connection, Dunn and Meyer(1997) introducedstructurally free logics in whichintroduction rules for combinators replace structuralrules—hence the label for these logics. Bimbó and Dunn(2014) introduced a technique to generate a combinatory inhabitant fortheorems of $T_\rightarrow$ from their standard proofs in thesequent calculus, which is used in the decision procedure for$T_\rightarrow^\textbf{t}$. Sequent calculuses provide bettercontrol over proofs than natural deduction or axiomatic systems do.The combinatory extraction procedure of Bimbó and Dunn (2014)yields an effective link between combinators and types grounded insequent calculus proofs, which obviates the apparent advantage of$\textrm{TA}_\textrm{CL}$ and axiomatic systems.

The rule of substitution is built-in into the formulation of$\textrm{TA}_\textrm{CL}$ via the ruleschema calleddetachment and the axiomschemas for the basic combinators. Itis obvious that there are formulas ofleast complexity that aretypes of $\textsf{S}$ and $\textsf{K}$, such that all the othertypes of $\textsf{S}$ and $\textsf{K}$ are their substitutioninstances. A formula that has this property is called aprincipaltype of a combinator. Obviously, a combinator that has a principaltype, has denumerably many principal types, which are all substitutioninstances of each other; hence, it is justified to talk about theprincipal type schema of a combinator. The existence ofprincipal types for complex combinators is not obvious, nevertheless,obtains.

Theorem. If the term $M$ is typable, then $M$ has aprincipal type and a principal type schema.

Principal types and principal type schemas may seem now to beinterchangeable everywhere. Thus we could take a slightly differentapproach and define $\textrm{TA}_\textrm{CL}$ to include axioms andthe rule schema of detachment together with therule ofsubstitution. This version of $\textrm{TA}_\textrm{CL}$ wouldassume the following form.

\[\Delta\vdash\textsf{S}\colon(p \rightarrow q\rightarrow s)\rightarrow(p\rightarrow q)\rightarrow p\rightarrow s\] \[\Delta\vdash\textsf{K}\colon q\rightarrow s\rightarrow q\] \[\frac{\Delta\vdash M\colon A\rightarrow B\qquad \Theta\vdash N\colon A} {\Delta,\Theta\vdash MN\colon B}\]\[\frac{\Delta\vdash M\colon A} {\Delta[P/B]\vdash M\colon A[P/B]}\]

where $P$ ranges over propositional variables. (The substitutionnotation is extended—in the obvious way—to sets of typeassignments.) Clearly, the two deduction systems are equivalent.

If substitution were dropped altogether, then the applicability ofdetachment would become extremely limited, for instance,$\textsf{SK}$ no longer would be typable. A compromise betweenhaving substitution everywhere and having no substitution at all is tomodify the detachment rule so that that includes as much substitutionas necessary to ensure the applicability of the detachment rule. Sucha rule (without combinatory terms or type assignments) was invented inthe 1950s by Carew A. Meredith, and it is usually calledcondenseddetachment. The key to the applicability of detachment is to finda common substitution instance of the minor premise and of theantecedent of the major premise. This step is calledunification. (A bit more formally, let $s(A)$ denote theapplication of the substitution $s$ to $A$. Then, the result ofthe condensed detachment of $A$ from $B\rightarrow C$ is $s(C)$,when there is an $s$ such that $s(A)= s(B)$, and for any $s_1$with this property, there is an $s_2$ such that $s_1$ is thecomposition of $s$ and $s_2$.)

Notice that it is always possible to choose substitution instances ofa pair of formulas so that the sets of their propositional variablesare disjoint, because formulas are finite objects. Themost generalcommon instance of two formulas $A$ and $B$ (that do not sharea propositional variable) is $C$, where $C$ is a substitutioninstance of both $A$ and $B$, and propositional variables areidentified by the substitutions only if the identification isnecessary to obtain a formula that is a substitution instance of both$A$ and $B$. Theunification theorem (specialized to simpletypes) implies that if two formulas $A$ and $B$ have a commoninstance then there is a formula $C$ such that all the commoninstances of $A$ and $B$ are substitution instances of $C$.Obviously, a pair of formulas either has no common instance at all, orit has $\aleph_0$ many most general common instances.

A famous example of a pair of formulas that haveno commoninstance is $A\rightarrow A$ and $A\rightarrow A\rightarrowB$. The instances $p \rightarrow p$ and $q\rightarrow q\rightarrowr$ share no propositional variables, however, neither $q\rightarrowq$ nor $(q\rightarrow r)\rightarrow q\rightarrow r$ matches theshape of the second formula. To put the problem differently, $q$ and$q\rightarrow r$ would have to be unified, but they cannot beunified no matter what formula is substituted for $q$. An immediateconsequence of this is that $\textsf{WI}$ is not typable.

On the other hand,

\[(r\rightarrow r)\rightarrow r\rightarrow r\]

and

\[((s\rightarrow s)\rightarrow s\rightarrow s)\rightarrow (s \rightarrows)\rightarrow s\rightarrow s\]

are substitution instances of $p\rightarrow p$ and of $q\rightarrowq$. Furthermore, all simple types are substitution instances of apropositional variable, hence $\textsf{II}$ can be assigned both thetype $r\rightarrow r$ and the type ($s\rightarrow s)\rightarrows\rightarrow s$—and, of course, the latter happens to be aninstance of the former because $A\rightarrow A$ is the principaltype schema of $\textsf{II}$. If we apply condensed detachment to$p\rightarrow p$ and $q\rightarrow q$, then we get $q\rightarrowq$ (via the substitutions $[p/q\rightarrow q]$ and $[q/q])$, andso condensed detachment yields the principal type of $\textsf{II}$.Incidentally, $\textsf{II}$ and $\textsf{I}$ provide an excellentexample to illustrate thatdistinct terms may have thesame principal type schema.

Condensed detachment has been used extensively to refineaxiomatizations of various implicational logics, especially, in searchfor shorter and fewer axioms. Some logics may be formulated usingaxioms (rather than axiom schemas) together with the rule of condenseddetachment—without loss of theorems. All the logics that wementioned so far ($J_{\rightarrow}$, $R_{\rightarrow}$,$T_{\rightarrow}$ and $E_{\rightarrow}$) are$\mathbf{D}$-complete, that is, they all may be axiomatizedby axioms and the rule of condensed detachment. That is, theimplicational fragments of classical and intuitionistic logics, andthe implicational fragments of the relevance logics $R$, $E$ and$T$ are all $\mathbf{D}$-complete. (See Bimbó (2007) forsome further technical details.)

Simply typed systems have been extended in various directions. Logicsoften contain connectives beyond implication. It is a naturalmodification of a type assignment system to expand the set of typesvia including furthertype constructors. Conjunction and fusionare the easiest to explain or motivate as type constructors, however,disjunction and backward implication have been introduced into typestoo. Types are useful, because they allow us to get a grip on classesof terms from the point of view of their behavior with respect toreduction.

Tait’s theorem. If a combinatory term $M$ is typable(with simple types) then $M$ strongly normalizes, that is, allreduction sequences of $M$ are finite (i.e., terminate).

The converse of this claim is, obviously, not true. For example,$\textsf{WI}$ strongly normalizes but untypable, because theantecedent of contraction cannot be unified with any instance ofself-implication. The aim to extend the set of typable terms led tothe introduction of $\land$ into types.

3.2 Intersection types

A different way to look at the problem of typing $\textsf{WI}$ is tosay that $\textsf{W}$ should have a type similar to the formula$(A\rightarrow (A\rightarrow B))\rightarrow A\rightarrow B$, but inwhich the formulas in place of the two formulas $A$ and$A\rightarrow B$ in the antecedent can be unified. This is themotivation for the inclusion of conjunction ($\land$) and top($\top$) as new type constructors.

An extended type system, that is often called theintersection typediscipline, is due to Mario Coppo and MariangiolaDezani-Ciancaglini. The set ofintersection types (denoted bywff) is defined as follows.

$p\in\textrm{wff}$ if $p$ is a propositional variable;
$\top\in\textrm{wff}$, where $\top$ is a constantproposition;
$A, B\in\textrm{wff}$ implies $(A\rightarrow B),(A\land B)\in\textrm{wff}$.

Of course, if TA$_\textrm{CL}$ is augmented with an expanded set oftypes, then new instances of the previously assigned types becomeavailable. However, the gist of having types with the new typeconstructors $\land$ and $\top$ is that the set of types has aricher structure than the relationships between types determined bythe rules of substitution and modus ponens.

The structure of intersection types is described by theconjunction–implication fragment of $B$, thebasicrelevance logic. In the following presentation of this logic,$\le$ is the main connective (an implication) of a formula and$\Rightarrow$ separates the premises and the conclusion of aninference rule.

\[\begin{align*}A\le A\qquadA\le\,&\,\top\qquad\top\le\top\to\top\\A\le A\land A\qquad A\land B&\;\le A\qquad A\land B\le B\\A\le B,\,B\le C&\;\Rightarrow A\le C \\A\le B,\,C\le D\Rightarrow&\; A\land C\le B\land D \\(A\rightarrow B)\land(A\rightarrow C)\le&\;(A\rightarrow(B\land C)) \\A\le B,\,C\le D\Rightarrow&\; B\rightarrow C\le A \rightarrow D\end{align*}\]

The axiom schemas for the combinators $\textsf{S}$, $\textsf{K}$and $\textsf{I}$ are as follows. Note that the axiom for$\textsf{S}$ is not simply a substitution instance (with newconnectives included) of the previous axiom for $\textsf{S}$.

\[\Delta\vdash\textsf{S}\colon(A\rightarrow B\rightarrow C)\rightarrow(D\rightarrow B)\rightarrow(A\land D)\rightarrow C\] \[\Delta\vdash \textsf{K}\colon A\rightarrow B\rightarrow A \qquad\Delta\vdash \textsf{I}\colon A\rightarrow A\]

There are four new rules added, and there is an axiom for$\top$.

\[\frac{\Delta\vdash M\colon A\quad\Delta\vdash M\colon B} {\Delta\vdash M\colon A\land B}\quad\frac{\Delta\vdash M\colon A\land B} {\Delta\vdash M\colon A}\quad\frac{\Delta\vdash M\colon A\land B} {\Delta\vdash M\colon B}\] \[\frac{\Delta\vdash M\colon A\qquad A\le B} {\Delta\vdash M\colon B}\quad\Delta\vdash M\colon\top\]

This type assignment system is equivalent to the intersection typeassignment system for the $\lambda$-calculus, and it allows a moreprecise characterization of classes of terms with respect to thetermination of reduction sequences.

Theorem.
(1) A term $M$ normalizes whenever $M$ is typable.
(2) A term $M$ strongly normalizes whenever $M$ is typable and theproof does not contain $\top$.

4. Models

CL has various kinds of models, three of which are exemplified in somedetail in this section.Algebraic models (often called“term models”) may be constructed without difficulty forboth the inequational and the equational systems of CL that wereintroduced in section 2.1. The set of terms forms an algebra, andgiven a suitable equivalence relation (that is also a congruence), theapplication operation can be lifted to the equivalence classes ofterms in the standard way. The quasi-inequational characterization ofthe so obtained algebra provides the basis for an algebraic semanticsfor these logics. Isolating the Lindenbaum algebra and verifying thatit is not a trivial algebra constitutes a consistency proof for$\text{CL}_\triangleright$ and $\text{CL}_=$.

4.1 Scott’s models

Dana Scott defined $P\omega$ and $D_\infty$ for the$\lambda$-calculus. We first outline $P\omega$—the so-calledgraph model, which is easier to understand.

The natural numbers have a very rich structure. $P\omega$ is thepower set of the set of natural numbers and it is at the core of themodel bearing the same label. Every natural number has a uniquerepresentation inbase $2$. (E.g., $7_{10}$ is $111$,that is, $7=1\cdot2^2+1\cdot2^1+1\cdot 2^0=4+2+1$.) Each binaryrepresentation is of the form

\[b_m\cdot2^m+b_{m-1} \cdot2^{m-1}+\cdots+b_1\cdot 2^1+b_0\cdot2^0 ,\]

where each $b$ is $0$ or $1$. Then each binary number may beviewed as the characteristic function of afinite subset of naturalnumbers. (On the left, there are infinitely many zeros, as in$\ldots000111$, which are omitted.) For a natural number $n$,$e_n$ denotes the corresponding finite set of natural numbers.(E.g., $e_7=\{0,1,2\}$.)

Thepositive topology on $P\omega$ comprises finitelygenerated open sets. Let $E$ denote the finite subsets of$\omega$. $X\subseteq P\omega$ is open iff $X$ is a cone (withrespect to $\subseteq$) generated by a subset of $E$. Given thepositive topology, a function $f\colon P\omega\rightarrow P\omega$turns out to becontinuous (in the usual topological sense) iff$f(x)=\cup\{f(e_n)\colon e_n\subseteq x\}$, where $e_n\in E$. Thismeans that $m\in f(x)$ iff $\exists e_n\subseteq x.\, m\inf(e_n)$, which leads to a characterization of a continuous function$f$ by the pairs of natural numbers $(n,m)$.

A one-one correspondence between (ordered) pairs of natural numbersand natural numbers is defined by

\[(n,m) = \frac{[(n+m)\cdot(n+m+1)]+2\cdot m} {2}\]

The set of pairs that constitute a (unary) function is sometimescalled thegraph of the function. The graph of a continuousfunction $f\colon P\omega\rightarrow P\omega$ is defined by$\textrm{graph}(f)=\{(n,m)\colon m\in f(e_n)\}$. In order to be ableto model type-free application—includingself-application—subsets of $\omega$ should be viewed asfunctions too. For $x, y\subseteq\omega$, the function determined by$y$ is defined as $\textrm{fun}(y)(x)=\{m\colon \existse_n\subseteq x.\,(n,m)\in y\}$. For a continuous function $f$,$\textrm{fun}(\textrm{graph}(f))=f$ holds.

The graph model of CL maps terms into subsets of $\omega$. To startwith, the combinators have concrete sets as their interpretations. Asa simple example, $\textsf{I}= \{(n,m)\colon m\in e_n\}$. Of course,each pair corresponds to an element of $\omega$, hence, we get a setof natural numbers. In particular, some of the elements are$\{1,6,7,11,15,23,29,30, \ldots\}$.

If the combinators (as well as the variables) are interpreted assubsets of $\omega$, then function application should take the firstset (viewed as a function of type $P\omega\rightarrow P\omega)$ andapply that to the second set. $\textrm{fun}(y)$ is a suitablefunction that is determined by $y \subseteq\omega$. In general, if$M$ and $N$ are CL-terms, and $I$ is the interpretation ofatomic terms into $P\omega$, then $I$ is extended to compoundterms by $I(MN)=\textrm{fun}(I(M))(I(N))$. (E.g., let $I(x)$ be$e_9=\{0,3\}$.$I(\textsf{I}x)=\textrm{fun}(I(\textsf{I}))(I(x))=\{m\colon \existse_n\subseteq I(x).\,(n, m)\in I(\textsf{I})\}$. We know what $I(\textsf{I})$ and $I(x)$ are; hence, we get further that$I(\textsf{I}x)= \{m\colon\exists e_n\subseteq e_9.\,m\in e_n\}$. Ofcourse, $\{0,3\}\subseteq \{0,3\}$, and so we have that$I(\textsf{I}x)=\{0,3\}$.) This model supports anintensionalnotion of functions.

The earliest model for atypefree applicative system as afunction space was also given by Scott, a couple of yearsbefore the graph model, in the late 60s. The following is an outlineof some of the key elements of the construction.

In pure typefree CL, an expression of the form $MM$ is a well-formedterm. Moreover, terms of this form can enter into provable equationsand inequations in multiple ways. For example, $xx=xx$ is an axiom,and by one of the rules, $y(xx)=y(xx)$ is provable too. A moreinteresting occurrence of a term of the form $MM$ can be seen in theprovable inequation $\textsf{S}(\textsf{SKK})(\textsf{SKK})x\triangleright xx$.

The set-theoretic reduction of a function yields a set of pairs (ingeneral, a set of tuples). In set theory (assuming well-foundedness,of course) a pair (e.g., $\{\{ a\},\{ a,b\}\}$) is never identicalto either of its two elements. Therefore, the main question concerninga mathematical model of CL is how to deal withself-application.

Scott’s original model is built starting with acompletelattice $(D, \le)$. That is, $(D,\le)$ is a partially orderedset in which greatest lower bounds (infima) and least upper bounds(suprema) exist for arbitrary sets of elements. A function $f$ from$(D,\le)$ into a complete lattice $(E,\le)$ is said to becontinuous when it preserves the supremum of each ideal on$D$, where an ideal is an upward directed downward closedsubset.

Atopology may be defined on $D$ by selecting certainincreasing sets as the opens. More precisely, if $I$ is an ideal and$C$ is a cone, then $C$ is open iff $C\cap I \ne\emptyset$provided that $\bigvee I\in C$, that is, provided that the supremumof $I$ is an element of $C$. (For example, complements ofprincipal ideals are open.) $f$ turns out to be continuous in theusual topological sense, that is, the inverse image of an open set isopen, when $D$ and $E$ are taken together with their topologies.This motivates the earlier labeling of these functions as continuous.Notably, all continuous functions aremonotone.

For the purposes of modeling functions in CL, the interestingfunctions are those that are continuouson $D$. However,these functions by themselves are not sufficient to obtain a modelingof self-application, because none of them has as its domain a set offunctions—as $D$ is not assumed to be a function space. Thesolution starts with defining ahierarchy of function spaces$D_0$, $D_1$, $D_2,\ldots$ so that each function space $D_n$,is a complete lattice on which continuous functions may be defined(creating the function space $D_{n+1}$). The importance of selectingcontinuous functions is that the emerging function space has thesame cardinality as the underlying set, which allows us todefine embeddings between function spaces adjacent within thehierarchy.

The hierarchy of all the function spaces $D_n$ may be accumulatedtogether. A standard construction in model theory is to form thedisjoint union of structures. (Disjointness can always be guaranteedby indexing the carrier sets of the structures.) Scott defined$D_\infty$ to be thedisjoint union of the function spaces$D_n$, for all $n$, except that the extremal elements are“glued together.” (More formally, the top elements and thebottom elements of the function spaces, respectively, are identifiedwith each other.) $D_\infty$ is a complete lattice, and byTarski’s fixed point theorem, a continuous function that maps$D_\infty$ into $D_\infty$ has a fixed point, which implies that$D _\infty$ isisomorphic to $D_\infty\rightarrowD_\infty$.

The above construction may also be conceptualized in terms ofstrings andCartesian products. The back-and-forth movesbetween functions of one and more than one variable—the“uncurrying” and “currying” offunctions—algebraically corresponds to the two directions ofresiduation. For example, a function $f\colon A\timesB\rightarrow C$ may be represented by a function $f^\prime\colon A\rightarrow B\rightarrow C$, and vice versa. Thus, without loss ofgenerality, it is sufficient to consider unary functions. If $a$ isa fixed element of the function space $D_\infty$, then $x = (a,x)$holds when $x$ is the fixed point of $a$. In terms of tuples, thesolution may be viewed as the infinite tuple $(a,(a,(a,\ldots$.

4.2 Relational semantics

A further model that we briefly outline falls into the set-theoreticalsemantics paradigm ofnonclassical logic and it is due to J.Michael Dunn and Robert K. Meyer (see Dunn and Meyer (1997)). CL and$\lambda$-calculuses are inherently connected to intuitionistic,relevance and other nonclassical logics. In particular, the$\text{CL}_\triangleright$ and $\text{CL}_=$ calculuses arenonclassical logics themselves. Set theoretical semantics in which theintensional connectives are modeled from relations on a collection ofsituations have been the preferred interpretation of nonclassicallogics since the early 1960s. These sorts of semantics are sometimescalled “Kripke semantics” (because Kripke introducedpossible-world semantics for some normal modal logics in 1959) or“gaggle semantics” (after the pronunciation of theabbreviation ‘ggl’ that stands for “generalizedGalois logics” introduced by Dunn (1991)).

A model for $\text{CL}_\triangleright$ may be defined as follows.Let ($W,\le, R,S,K,v)$ comprise a (nonempty) partially ordered set$(W,\le)$ with a three-place relation $R$ on $W$, and let $S$,$K\in W$. Furthermore, for any $\alpha,\beta,\gamma,\delta\in W$,the conditions (s) and (k) are true.

(s): $\exists \zeta_1,\zeta_2,\zeta_3\in W.\,RS\alpha\zeta_1\landR\zeta_1 \beta\zeta_2\land R\zeta_2\gamma\delta\quad$ implies
$\exists\zeta_1,\zeta_2,\zeta_3\in W.\,R\alpha\gamma\zeta_1\landR\beta\gamma\zeta_2\land R\zeta_1\zeta_2\delta$,
(k): $\exists\zeta_1\in W.\,RK\alpha\zeta_1\landR\zeta_1\beta\gamma\quad$ implies $\quad\alpha\le\gamma.$

The ternary relation is stipulated to be antitone in its first twoargument places and monotone in the third. These components define aframe for $\text{CL}_\triangleright$. The valuation function $v$maps variables $x,y,z, \ldots$ into (nonempty) cones on $W$, andit maps the two primitive combinators $\textsf{S}$ and$\textsf{K}$ into the cones generated by $S$ and $K$,respectively. Recall, that the standard notation in CL hidesapplication, a binary operation that allows forming compound terms.The next clause extends $v$ to compound terms and makes thisoperation explicit again.

\[v(MN)=\{\beta\colon\exists\alpha,\gamma.\,R\alpha\gamma\beta\land\alpha\in v(M)\land\gamma\in v(N)\}\]

An inequation $M\triangleright N$ is valid if $v(M)\subseteq v(N)$under all valuations on frames for $\text{CL}_\triangleright$. (Thatis, the relationship between the interpretations of the two terms isinvariant whenever $v$ is varied on the set of variables.)

Informally, the underlying set $W$ is a set ofsituations,and $R$ is anaccessibility relation connecting situations.All the terms are interpreted as sets of situations, and functionapplication is theexistential image operation derived from$R$. A difference from the previous models is that the result of anapplication of a term to a term is not determined by the objectsthemselves that interpret the two terms—rather the applicationoperation is defined from $R$.

This semantics generalizes the possible worlds semantics for normalmodal logics. Therefore, it is important to note that the situationsarenot maximally consistent theories, rather they are theoriespossessing the property that for any pair of formulas they contain aformula that implies both of them. Equivalently, the situations may betaken to be dual ideals on the Lindenbaum algebra of$\text{CL}_\triangleright$. These situations are typicallyconsistent in the sense that they do not contain all the terms in allbut one case. (The notion of negation consistency, of course, cannotbe defined for $\text{CL}_\triangleright$ or for$\text{CL}_=$.)

Relational semantics can be defined for $\text{CL}_=$ along similarlines. Then soundness and completeness—that is, the followingtheorem—obtains.

Theorem.
(1) An inequation $M\triangleright N$ is provable in$\text{CL}_\triangleright$ if and only if $v(M)\subseteq v(N)$ inany model for $\text{CL}_\triangleright.$
(2) An equation $M = N$ is provable in $\text{CL}_=$ if and onlyif $v(M)=v(N)$ in any model for $\text{CL}_=.$

Relational and operational semantics for systems of CL that includedual and symmetric combinators can be found in Bimbó(2004).

5. Computable functions and arithmetic

A remarkable feature of CL is that despite its seeming simplicity itis apowerful formalism. Of course, the strength of CL cannotbe appreciated without discovering certain relationships betweencombinatory terms or without an illustration that computable functionsare definable.

An important beginning step in the formalization of mathematics is theformalization of arithmetic, that was first achieved by the Dedekind–Peano axiomatization. There are various ways to formalize arithmetic in CL;two representations of numbers are described in this section togetherwith some functions on them.

Numbers may be thought to be objects (or abstract objects) ofsome sort. (Here by numbers we mean natural numbers, that is, $0$and the positive integers.) Numbers could be characterized, forexample, by thestructure they possess as a set. This structuresupports properties such as $0\ne1$, and that the sum of $n$ and$m$ is the same number as the sum of $m$ and $n$. Anotherwell-known property of the natural numbers is, for example, theexistence of infinitely many prime numbers.

Numbers can be represented in CL by terms, and one way is to choosethe terms $\textsf{KI}$, $\textsf{I}$, $\textsf{SBI}$,$\textsf{SB} (\textsf{SBI}),\ldots$ for $0$, $1$, $2$, $3$,etc. The terms that represent the arithmetic operations vary,depending on which terms stand for the numbers. Note that unlike theDedekind–Peano formalization of arithmetic, CL makes nosyntactic distinction that would parallel the difference betweenindividual constants and function symbols—in CL the only objectsare terms. The above list of terms already shows thesuccessorfunction, which is $\textsf{SB}$. ($\textsf{SB}(\textsf{KI})$strongly equals to $\textsf{I}$, that is, $1$ is the successor of$0$.)

Addition is the term $\textsf{BS}(\textsf{BB})$, andmultiplication is the term $\textsf{B}$. The usual recursivedefinition of multiplication based on addition may suggest thataddition should be a simpler operation than multiplication. However,in CL the numbers themselves are functions, and so they haveproperties that allows $\textsf{B}$—a simpler lookingterm—to be chosen for the function that is often perceived to bemore complex than addition. (The addition operation could be definedusing primitive recursion, which would produce a more complex term.)As a classical example, we may consider the term $\textsf{BII}$,that is strongly equal to $\textsf{I}$, that is,$1\times1=1$—as expected. We do not pursue here this numericalrepresentation further. We only note that the shape of these numbersis closely related to Church’s numerals in the$\lambda$-calculus, each of which is a binary function (whereashere, each number is a unary function).

Another way to represent numbers in CL is to start with a differentchoice of terms for the numbers. Previously, $\textsf{I}$ stood for$1$, now we take $\textsf{I}$ to be $0$. The successor of anumber $n$ is $\textsf{V} (\textsf{KI})n$, where the secondoccurrence of $n$ indicates a numeral, that is, the combinator thatrepresents $n$. (The numeral for $n$ is often denoted—moreprecisely—by an overlined or otherwise decorated $n$. However,the double usage of $n$ in a limited context should not cause anyconfusion.) In other words, thesuccessor function is$\textsf{V}(\textsf{KI})$. Notice that the numbers in the presentrepresentation are terms over a more restricted combinatory base thanin the former case. For example, no combinator with duplicative effectis definable from $\{\textsf{I},\textsf{K},\textsf{V}\}$.

Some simplerecursive functions may be defined as follows. Thepredecessor function $P$ on numbers is “$-1$”(i.e., subtracting one) for all numbers greater than or equal to$1$, and the predecessor of $0$ is set to be $0$. The next termdefines the predecessor function which is abbreviated by $P$.

\[P=\textsf{C}(\textsf{W}(\textsf{BB}(\textsf{C}(\textsf{TK})\textsf{I})))(\textsf{KI})\]

If $n$ is a numeral, then $Pn$ reduces to $n\textsf{KI}(n(\textsf{KI}))$, which suggests that for positive numbers, $P$ couldhave been defined to be the term $\textsf{T}(\textsf{KI})$, because$\textsf{T}(\textsf{KI})n$ reduces to $n-1$ whenever $n$ is aterm of the form $\textsf{V}(\textsf{KI})(n-1)$.

Some models of computation (such as register machines) and certainprogramming languages include atest for zero as a primitiveconstruct. It is useful to find a CL-term for a function $Z$ suchthat $Znxy$ reduces to $x$ if $n$ is zero, whereas $Znxy$reduces to $y$ when $n$ is positive. $Znxy$ may be thought of asthe conditional instruction “If $n=0$ then $x$ else$y$,” where $x$ and $y$ are themselves functions. (Ofcourse, in the pseudo-code one should have assumed that $n$ is ofinteger type and cannot take a negative value, that could beguaranteed by a declaration of variables and an additional conditionalstatement.) The following definition works for branching on zero.

\[Z=\textsf{TK}\]

$\textsf{TK}nxy=n\textsf{K}xy$, and if $n$ is zero, that is, $n=\textsf{I}$, then by another step $\textsf{K}xy$ and then $x$results; whereas if $n$ is positive, then after a few morereductions, one gets $\textsf{KI}xy$, that is, $y$. The two terms,$\textsf{K}xy$ and $\textsf{KI}xy$, hint toward an interpretationof $\textsf{K}$ and $\textsf{KI}$ astruth andfalsity, or they can be viewed as terms that can select,respectively, the first or the second argument. These ideas may befurther developed into definitions of truth functions and arepresentation of tuples.

Addition may be defined by the recursive equation $+mn=Zmn(\textsf{V}(\textsf{KI})(+(Pm)n))$, where $m$ and $n$ arenumerals, and $P$ and $Z$ are the already defined functions. (Theabbreviations are used to enhance the readability of theterms—they can be replaced everywhere by the definingcombinators.) To put into words, if $m$ is $0$ then the sum is$n$, otherwise $m+n$ is the successor of $(m-1)+n$. Of course,this definition closely simulates the definition of addition fromrecursion theory, where addition is often defined by the two equations$+(0,n)=n$ and $+(s(m),n)=s(+(m,n))$ (with $s$ denoting thesuccessor function). The fact that CL can express addition in thisform shows—once again—the versatility of CL.

Combinatorial completeness guarantees that the term on the right handside of the defining equation for $+$ (i.e., the term$Zmn(\textsf{V}(\textsf{KI}) (+(Pm)n)))$ can be transformed into aterm in which $+$ is the first, $m$ and $n$ are the second andthird arguments, respectively. Then $+$ can be defined explicitly asthe fixed point of the combinator

\[\textsf{B}(\textsf{BW})(\textsf{BW}(\textsf{B}(\textsf{B}(\textsf{C}(\textsf{BB}(\textsf{BC}(\textsf{TK})))))(\textsf{B}(\textsf{B}(\textsf{B}(\textsf{V}(\textsf{KI}))))(\textsf{CB}(\textsf{T}(\textsf{KI})))))).\]

Of course, we can abbreviate the so obtained term as $+$ for thesake of transparency, just as we used earlier $P$ and $Z$ asshorthands for longer combinatory terms.

Multiplication is often denoted by $\,\cdot\,$. The recursiveequation $\,\cdot\, mn = Zm\textsf{I}(+n(\,\cdot\,(Pm)n))$ definesmultiplication and it can be deciphered as “if $m$ is $0$then the result is $0$, else $n$ is added to the result of$(m-1)\cdot n$.” The next step in the definition brings theright-hand side term to the form $\textsf{X}\cdot mn$, where$\textsf{X}$ does not contain occurrences of $\,\cdot\,$, $m$ or$n$. Then taking the fixed point of $\textsf{X}$, and setting$\,\cdot\,$ to be $\textsf{YX}$ concludes the definition of themultiplication function. For instance, the abstraction can yield thecombinator

\[\textsf{BW}(\textsf{B}(\textsf{B}(\textsf{C}(\textsf{BB}(\textsf{C}(\textsf{TK})\textsf{I}))))(\textsf{B}(\textsf{BW})(\textsf{B}(\textsf{B}(\textsf{B}(\textsf{C}+)))(\textsf{CB}(\textsf{T}(\textsf{KI})))))).\]

Thefactorial function is definable from the predecessorfunction plus from multiplication, and it is useful e.g., incombinatorics. The factorial function (denoted by $\,!\,$) isrecursively definable by the equation $\,!\,m=Zm(\textsf{V}(\textsf{KI})\textsf{I})(\cdot m(\,! \,(Pm)))$, thatmay be read as “if $m$ is $0$, then $\,!\, m=1$, otherwise$\,!\, m$ equals to $m$ multiplied by the factorial of$m-1$.”

Of course, it is not necessary to define various numerical functionsby simulating their recursive definitions. As we saw above in the caseof the first representation of numbers, we might just happen to havethe right terms such as $\textsf{BS}(\textsf{BB})$ and$\textsf{B}$, that behave as the target functions do on numbers.That is, an equally good way to define arithmetic functions is tosimply list some terms and then show that they behave as expected.However, once it has been shown that thebasic primitive recursivefunctions together withrecursion andminimizationcan be emulated in CL, we have got not only a nice collection ofarithmetic functions in the form of combinators to work with, but alsoa proof that combinatory logic is sufficiently expressive to formalizeallpartial recursive functions. Indeed, the remaining steps ofsuch a proof can be carried out in CL, though the details are beyondthe scope of this entry.

5.1 Gödel sentence

The abbreviations and the interspersed explanations in the sketchabove may obscure that arithmetic has been formalized in a languagethat consists of five symbols (when juxtaposition is not counted):$\textsf{S}$, $\textsf{K}$, $=$ plus two delimiters, $\,(\,$and $\,)\,$. The finite (and perhaps, surprisingly small) number ofsymbols and the availability of recursive functions conjure thethought that an arithmetization of the syntax of CL could beattempted.

Gödel achieved an encoding of a formal language by assigning numbers tosymbols, formulas and sequences of formulas, which later became knownas “Gödel numbers.” Concretely, Gödel assignedodd numbers to symbols and products of powers of primes (with thenumber corresponding to a symbol in the exponent) to sequences ofsymbols. However, it is possible to arithmetize the language of CLwithout placing a strong emphasis on the existence and the propertiesof prime numbers. (See for example, Raymond M. Smullyan’s books:Smullyan (1985) and Smullyan (1994).) The five symbols get as theirGödel numbers the first five positive integers. A string isassigned the number in base $10$ that results from the concatenationof the corresponding numbers for the symbols.

The following outline gives the flavor of an analogue ofGödel’s incompleteness theorem adapted to CL. It ispossible to define a combinator such that if this combinator isapplied to a numeral $n$, then the whole term reduces to the numeral$m$ that is the numeral denoting theGödel number of thenumeral $n$. Slightly more formally, there is a combinator$\delta$ such that $\delta n = G(n)$ (where $G (n)$ denotes theGödel number of the expression $n$). Furthermore, there is acombinatory term, which returns the numeral itself followed by$G(n)$, when applied to a numeral $n$. For any term $A$ there isa term $B$ such that the equation $A(\delta B)=B$ is true. Thisstatement (or its concrete variant for a particular formal system) isusually called thesecond fixed point theorem. Computablecharacteristic functions of recursive sets of numbers can berepresented by combinators with the choice of $\textsf{K}$ for truthand $\textsf{KI}$ for falsity. The complements of such functions arecomputable too. Finally, it can be proved that there is no combinatorthat represents the set ofall true equations. To put itdifferently, any combinator either represents a set of equations thatfails to include some true equations, or represents a set of equationsthat includes all true but also some false equations.

Alonzo Church proved theundecidability of classical first-order logicrelying on Gödel’s incompleteness theorem. Dana Scottproved that if $A$ is a nonempty proper subset of $\lambda$-termsthat is closed under equality then $A$ is not recursive. Theanalogous claim for CL, that follows from the existence of aGödelian sentence for CL, is that it isundecidable if twoCL-terms are equal.

Bibliography

Due to obvious limitations of size, only some representativepublications are listed here. More comprehensive bibliographies may befound in Curry, Hindley and Seldin (1972), Hindley (1997), Anderson,Belnap and Dunn (1992), Terese (2003) as well as Hindley and Seldin(2008).

Anderson, A., N. Belnap, and J.M. Dunn, 1992.Entailment: TheLogic of Relevance and Necessity (Volume II), Princeton:Princeton University Press.
Barendregt, H. P., 1981.The Lambda Calculus. Its Syntax andSemantics, (Studies in Logic and the Foundations of Mathematics:Volume 103), Amsterdam: North-Holland.
Barendregt, H., J. Endrullis, J. W. Klop and J. Waldmann, 2017.“Dance of the starlings,” in M. Fitting and B. Rayman(eds.),Raymond Smullyan on Self Reference, (OutstandingContributions to Logic: Volume 14), Cham: Springer Nature,67–111.
Bimbó, K., 2003. “The Church-Rosser property in dualcombinatory logic,”Journal of Symbolic Logic, 68:132–152.
–––, 2004. “Semantics for dual andsymmetric combinatory calculi,”Journal of PhilosophicalLogic, 33: 125–153.
–––, 2005. “Types of $\textsf{I}$-freehereditary right maximal terms,”Journal of PhilosophicalLogic, 34: 607–620.
–––, 2007. “Relevance logics,” in D.Jacquette (ed.),Philosophy of Logic (Handbook of thePhilosophy of Science: Volume 5), D. Gabbay, P. Thagard and J. Woods(eds.), Amsterdam: Elsevier/North-Holland, 2007, pp.723–789.
–––, 2010. “Schönfinkel-typeoperators for classical logic,”Studia Logica, 95:355–378.
–––, 2012.Combinatory Logic: Pure, Appliedand Typed, Boca Raton, FL: CRC Press.
–––, 2014.Proof Theory: Sequent Calculi andRelated Formalisms, Boca Raton, FL: CRC Press.
–––, 2018. “Inhabitants of intuitionisticimplicational theorems,” in L. S. Moss, R de Queiroz and M.Martinez (eds.),Logic, Language, Information and Computation.Proceedings of the 25th International Workshop, WoLLIC 2018,Bogota, Colombia, July 24–27, 2018 (Lecture Notes in ComputerScience: Volume 10944), Berlin: Springer, pp. 1–24.
Bimbó, K., and J. M. Dunn, 2008.Generalized GaloisLogics. Relational Semantics of Nonclassical Logical Calculi(CSLI Lecture Notes: Volume 188), Stanford, CA: CSLIPublications.
–––, 2012. “New consecution calculi for$R^\textbf{t}_\rightarrow$,”Notre Dame Journal of FormalLogic, 53: 491–509.
–––, 2013. “On the decidability ofimplicational ticket entailment,”Journal of SymbolicLogic, 78: 214–236
–––, 2014. “Extracting $\textsf{BB'IW}$inhabitants of simple types from proofs in the sequent calculus$LT^{\mathbf{t}}_{\rightarrow}$ for implicational ticketentailment,”Logica Universalis, 8(2):141–164.
Broda, S., Damas, L., Finger, M. and P. S. Silve e Silva, 2004.“The decidability of a fragment of$\textsf{BB'IW}$-logic,”Theoretical ComputerScience, 318: 373–408.
Bunder, M. W., 1992. “Combinatory logic and lambda calculuswith classical types,”Logique et Analyse,137–128: 69–79.
–––, 2000. “Expedited Broda–Damasbracket abstraction,”Journal of Symbolic Logic, 65:1850–1857.
Cardone, F., and J. R. Hindley, 2006. “History oflambda-calculus and combinatory logic,” in D. M. Gabbay and J.Woods (eds.),Logic from Russell to Church (Handbook of theHistory of Logic: Volume 5), Amsterdam: Elsevier, 2006,732–817.
Church, A., 1941.The Calculi of Lambda-conversion, 1stedition, Princeton, NJ: Princeton University Press.
Coppo, M., and M. Dezani-Ciancaglini, 1980. “An extension ofthe basic functionality theory for the $\lambda$-calculus,”Notre Dame Journal of Formal Logic, 21: 685–693.
Curry, H. B., 1963.Foundations of Mathematical Logic,1st edition, New York: McGraw–Hill Book Company, Inc. (2ndedition, 1977, New York: Dover Publications, Inc.)
Curry, H. B., and R. Feys, 1958.Combinatory Logic(Studies in Logic and the Foundations of Mathematics: Volume I), 1stedition, Amsterdam: North-Holland.
Curry, H. B., J. R. Hindley, and J. P. Seldin, 1972.Combinatory Logic (Studies in Logic and the Foundations ofMathematics: Volume II), Amsterdam: North-Holland.
Dunn, J. M., 1991. “Gaggle theory: An abstraction of Galoisconnections and residuation with applications to negation,implication, and various logical operators,” in J. van Eijck(ed.),Logics in AI: European Workshop JELIA ’90(Lecture Notes in Computer Science: Volume 478), Springer, Berlin,1991, pp. 31–51.
Dunn, J. M., and R. K. Meyer, 1997. “Combinators andstructurally free logic,”Logic Journal of IGPL, 5:505–537.
Endrullis, J., J. W. Klop and A. Polonsky, 2016. “Reductioncycles in lambda calculus and combinatory logic,” in J. vanEijck, R. Iemhoff and J. J. Joosten (eds.),Liber AmicorumAlberti. A Tribute to Albert Visser (Tributes, Volume 30),London: College Publications, 111–124.
Fitch, F., 1942. “A basic logic,”Journal ofSymbolic Logic, 7: 105–114.
–––, 1942. “An extension of basiclogic,”Journal of Symbolic Logic, 13:95–106.
Gierz, G., K. H. Hofmann, K. Keimel, J. D. Lawson, M. W. Mislove,and D. S. Scott, 2003.Continuous Lattices and Domains(Encyclopedia of Mathematics and its Applications: Volume 93),Cambridge: Cambridge University Press.
Gödel, K., 1931. “Über formal unentscheidbareSätze derPrincipia mathematica und verwandter SystemeI,” in S. Feferman (ed.),Kurt Gödel: CollectedWorks (Volume I), New York and Oxford: Oxford University Pressand Clarendon Press, 1986, pp. 144–195.
Hindley, J. R., 1997.Basic Simple Type Theory (CambridgeTracts in Theoretical Computer Science: Volume 42), Cambridge:Cambridge University Press.
Hindley, J. R., and J. P. Seldin, 2008.$\lambda$-calculusand Combinators, an Introduction, Cambridge: Cambridge UniversityPress.
Kleene, S. C., 1967.Mathematical Logic, New York: JohnWiley & Sons, Inc; reprinted Mineola, NY: Dover, 2002.
Mackie, I., 2019. “Linear numeral systems,”Journal of Automated Reasoning, 63: 887–909.
Padovani, V., 2013. “Ticket Entailment is decidable,”Mathematical Structures in Computer Science, 23(3):568–607.
Quine, W. V. O., 1960. “Variables explained away,”Proceedings of the American Philosophical Association, 104(3): 343–347; reprinted in W.V.O. Quine,Selected LogicalPapers, New York: Random House, 1966, 227–235.
–––, 1981. “Predicate functorsrevisited,”Journal of Symbolic Logic, 46:649–652.
Révész, G. E., 1988.Lambda-calculus,Combinators and Functional Programming, Cambridge: CambridgeUniversity Press.
Rezus, A., 1982.A Bibliography of Lambda-Calculi, CombinatoryLogics and Related Topics, Amsterdam: Mathematisch Centrum.
Rosser, J. B., 1936. “A mathematical logic withoutvariables,”Annals of Mathematics, 2:127–150.
Schönfinkel, M., 1924. “On the building blocks ofmathematical logic,” in J. van Heijenoort, (ed.),From Fregeto Gödel. A Source Book in Mathematical Logic, Cambridge,MA: Harvard University Press, 1967, pp. 355–366.
Scott, D., 1970.Outline of a Mathematical Theory ofComputation (Technical report), Oxford: Oxford UniversityComputing Laboratory Programming Research Group.
–––, 1974. “The language Lambda,(abstract),”Journal of Symbolic Logic, 39:425–426.
–––, 1976. “Data types as lattices,”SIAM Journal on Computing, 5: 522–587.
Seldin J. P., 2006. “The logic of Curry and Church,”in D. M. Gabbay and J. Woods (eds.),Logic from Russell toChurch (Handbook of the History of Logic: Volume 5), Amsterdam:Elsevier, 2006, 819–873.
Smullyan, R. M., 1985.To Mock a Mockingbird. And other LogicPuzzles Including an Amazing Adventure in Combinatory Logic, NewYork: Alfred A. Knopf.
–––, 1994.Diagonalization andSelf-reference, Oxford: Clarendon.
Updike, E. T., 2010.Paradise Regained: Fitch’s Programof Basic Logic, Ph.D. Thesis, University of California Irvine,Ann Arbor, MI: ProQuest (UMI).
–––, 2012. “Abstraction in Fitch’sbasic logic,”History and Philosophy of Logic, 33:215–243.
Tait, W., 1967. “Intensional interpretations of functionalsof finite type I,”Journal of Symbolic Logic, 32:198–212.
Terese (by Marc Bezem, Jan Willem Klop, Roel de Vrijer, ErikBarendsen, Inge Bethke, Jan Heering, Richard Kennaway, Paul Klint,Vincent van Oostrom, Femke van Raamsdonk, Fer-Jan de Vries and HansZantema), 2003.Term Rewriting Systems (Cambridge Tracts inTheoretical Computer Science: Volume 55), Cambridge: CambridgeUniversity Press.
Wolfram, S., 2021.Combinators. A Centennial View,Champagne, IL: Wolfram Media Inc. [Wolfram 2021 available online]

Academic Tools

How to cite this entry.
Preview the PDF version of this entry at theFriends of the SEP Society.
Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

TLCA (Typed Lambda Calculi and Applications)open problem list
Wolfram S combinator challenge (and $20,000 prize)problem description
Combinatory Logic page atSoftware and Tutorials for Instruction in Symbolic Logicin New Zealand.
Roger B. Jones’s$\lambda$-calculus website
Chris Rathman’sList of combinatory definitions

Acknowledgements

I am grateful to the referees of the first edition—both to the“internal referees” of thisEncyclopedia and toJonathan P. Seldin—for their helpful comments and suggestions,as well as certain corrections. Heeding the advice of the referees, Irepeatedly tried to make the entry less technical and morereadable.

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free

Browse

About

Support SEP

Mirror Sites

View this site from another server:

USA (Main Site)Philosophy, Stanford University

Info about mirror sites

Library of Congress Catalog Data: ISSN 1095-5054

\(\textsf{S}xyz \mathbin{\triangleright_1} xz(yz)\)	\(\textsf{K}xy \mathbin{\triangleright_1} x\)	\(\textsf{I}x \mathbin{\triangleright_1} x\)
\(\textsf{B}xyz \mathbin{\triangleright_1} x(yz)\)	\(\textsf{T}xy \mathbin{\triangleright_1} yx\)	\(\textsf{C}xyz \mathbin{\triangleright_1} xzy\)
\(\textsf{W}xy \mathbin{\triangleright_1} xyy\)	\(\textsf{M}x \mathbin{\triangleright_1} xx\)	\(\textsf{Y}x \mathbin{\triangleright_1}x(\textsf{Y}x)\)
\(\textsf{J}xyzv \mathbin{\triangleright_1} xy(xvz)\)	\(\textsf{B}^\prime xyz \mathbin{\triangleright_1} y(xz)\)	\(\textsf{V}xyz \mathbin{\triangleright_1} zxy\)

\(M\triangleright M\)	\(\textsf{S}MNP\triangleright MP(NP)\)	\(\quad\textsf{K}MN\triangleright M\)
\(\dfrac{M\triangleright N \quad N\trianglerightP}{M\triangleright P}\)	\(\dfrac{M\triangleright N}{MP\triangleright NP}\)	\(\dfrac{M\triangleright N}{PM\triangleright PN}\)

\(M=M\)	\(\textsf{K}MN=M\)	\(\quad\textsf{S}MNP=MP(NP)\quad\)
\(\quad\dfrac{M=N \quad N=P}{M=P}\quad\)	\(\dfrac{M=N}{N=M}\)	\(\dfrac{M=N}{MP=NP}\)	\(\dfrac{M=N}{PM=PN}\)

\(\textsf{I}=\textsf{SK}(\textsf{KK})\)	\(\textsf{T}=\textsf{B}(\textsf{SI})\textsf{K}\)	\(\textsf{C}=\textsf{B}(\textsf{T}(\textsf{BBT}))(\textsf{BBT})\)
\(\textsf{W}=\textsf{CSI}\)	\(\textsf{M}=\textsf{SII}\)	\(\textsf{Y}=\textsf{BW}(\textsf{BB}^\prime\textsf{M})(\textsf{BW}(\textsf{BB}^\prime\textsf{M}))\)
\(\textsf{V}=\textsf{BCT}\)	\(\textsf{B}^\prime=\textsf{CB}\)	\(\textsf{J}=\textsf{W}(\textsf{BC}(\textsf{B}(\textsf{B}(\textsf{BC}))(\textsf{B}(\textsf{BB})(\textsf{BB}))))\)

\(\textsf{I}=\textsf{SKK}\)	\(\textsf{I}=\textsf{WK}\)	\(\textsf{I}=\textsf{CK}(\textsf{KK})\)
\(\textsf{B}=\textsf{CB}^\prime\)	\(\textsf{S}^\prime=\textsf{CS}\)	\(\textsf{S}=\textsf{CS}^\prime\)
\(\textsf{W}=\textsf{S}^\prime\textsf{I}\)	\(\textsf{W}=\textsf{B}(\textsf{T}(\textsf{BM}(\textsf{BBT})))(\textsf{BBT})\)	\(\textsf{W}=\textsf{C}(\textsf{S}(\textsf{CC})(\textsf{CC}))\)
\(\textsf{R}=\textsf{BBT}\)	\(\textsf{Y}=\textsf{BM}(\textsf{CBM})\)	\(\textsf{Y}=\textsf{B}^\prime(\textsf{B}^\prime\textsf{M})\textsf{M}\)

Movatterモバイル変換