\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{combinatory logic}

\hypertarget{combinatory_logic}{}\section*{{Combinatory logic}}\label{combinatory_logic}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{historical_remarks}{Historical remarks}\dotfill \pageref*{historical_remarks} \linebreak
\noindent\hyperlink{the_combinators_s_k_and_i}{The combinators S, K, and I}\dotfill \pageref*{the_combinators_s_k_and_i} \linebreak
\noindent\hyperlink{encoding_abstraction}{Encoding abstraction}\dotfill \pageref*{encoding_abstraction} \linebreak
\noindent\hyperlink{LinearAndAffine}{Linear (BCI) and affine (BCK) combinatory logic}\dotfill \pageref*{LinearAndAffine} \linebreak
\noindent\hyperlink{remark}{Remark}\dotfill \pageref*{remark} \linebreak
\noindent\hyperlink{related_pages}{Related pages}\dotfill \pageref*{related_pages} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

\begin{quote}%
Combinator algebra has always struck me as a subject almost impossible to watch: it's a lousy spectator sport but has a reputation of habit-forming as a participator sport. P. Freyd (\hyperlink{Freyd89}{1989}, p.63)


\end{quote}
\textbf{Combinatory logic} is a rephrasing of the [[lambda calculus]] that avoids explicit mention of [[variables]] and of [[lambda abstraction]]. Instead it uses [[combinators]] -- in the most common case, they are traditionally called $S$, $K$, and $I$ -- with the only other operation being [[application]].

Since this move circumvents the necessity of variable management, combinatory logic is important for applications in [[computer science]] and [[linguistics]].

Under the [[propositions as types]] correspondence, combinatory logic corresponds to the presentation of [[logic]] using a [[Hilbert system]] (instead of [[natural deduction]] or [[sequent calculus]]). There are versions of combinatory logic corresponding to [[linear logic]] and [[affine logic]], generally called \textbf{BCI logic} and \textbf{BCK logic} (after the combinators they use).

\hypertarget{historical_remarks}{}\subsection*{{Historical remarks}}\label{historical_remarks}

The 1920s gave birth to several formal systems that permitted to base mathematics on the notion of function like e.g. the lambda calculus or von Neumann `set' theory that eventually morphed into [[NBG|Neumann-Bernays-Gödel set theory]]. Notably the first of such systems was combinatory logic which was introduced by [[Moses Schönfinkel]] in 1920 (\hyperlink{Schoen24}{Sch\"o{}nfinkel 1924}) and developed (partly independently) by [[Haskell Curry]] by the end of the decade.

Of course, a later such function based approach to mathematics is [[category theory]] and there has been in fact some interaction between combinatory logic and category theory (\hyperlink{Bunder84}{Bunder 1984}). In 1972 when the connection between Cartesian closed categories and lambda calculus was an object of active research, [[Jim Lambek]] wrote:

\begin{quote}%
Sch\"o{}nfinkel's original program to base all of mathematics on combinatory logic can now be said to have been carried out by Lawvere in his many articles pursuing a categorical formulation of mathematics. (\hyperlink{Lambek72}{1972}, p.57)


\end{quote}
\hypertarget{the_combinators_s_k_and_i}{}\subsection*{{The combinators S, K, and I}}\label{the_combinators_s_k_and_i}

The basic combinators can be defined in terms of $\lambda$-calculus as

\begin{itemize}%
\item $S = \lambda x. \lambda y. \lambda z. (x z)(y z)$
\item $K = \lambda x. \lambda y. x$
\item $I = \lambda x. x$

\end{itemize}
In [[simply typed lambda-calculus]], these combinators are [[polymorphic]] with types

\begin{itemize}%
\item $S : (A \to (B\to C)) \to (A\to B) \to (A\to C)$
\item $K : A\to (B\to A)$
\item $I : A\to A$

\end{itemize}
for arbitrary types $A,B,C$.

When combinatory logic is presented on its own rather than in terms of $\lambda$-calculus, the combinators are characterized by reduction rules that mirror their definition in terms of $\lambda$-abstractions:

\begin{itemize}%
\item $S x y z \equiv (x z)(y z)$
\item $K x y \equiv x$
\item $I x \equiv x$

\end{itemize}
Sometimes the combinator $I$ is omitted, as it can be defined from $S$ and $K$ as $I=S K K$.

\hypertarget{encoding_abstraction}{}\subsection*{{Encoding abstraction}}\label{encoding_abstraction}

The combinators $S$, $K$, and $I$ are used to encode $\lambda$-abstraction in the following way. If $M$ is a term in combinatory logic (perhaps containing variables), we define $\lambda x.M$ by induction over the structure of the term $M$.

\begin{itemize}%
\item If $M=x$, then $\lambda x.x = I$.
\item If $M$ is a variable $y\neq x$, then $\lambda x.y = K y$.
\item If $M = N P$ is an application of one term to another, then $\lambda x.M = S (\lambda x.N) (\lambda x.P)$, so we can recursively translate $\lambda x.N$ and $\lambda x.P$.

\end{itemize}
(It is common to see this described with the second case given as ``$\lambda x.M = K M$ whenever $M$ does not contain $x$ as a [[free variable]]''. However, this overlaps with the third case and is not structurally recursive. The above definition translates $\lambda x.y z$ to $S(K y)(K z)$, while the one with the free-variable-check produces $K(y z)$; both reduce to $y z$ when applied to any argument.)

Using this construction of an ``abstraction operator'' in the combinatory logic, we can then proceed to translate an arbitrary term of $\lambda$-calculus into combinatory logic by translating all the abstractions ``from the inside out''. Formally, we crawl over the term and whenever we find an abstraction, we first recurse into its body, then we apply the above abstraction operator.

The construction of an abstraction operator in combinatory logic is analogous to a [[cut admissibility]] theorem; the resulting translation of $\lambda$-calculus into combinatory logic is then analogous to the corresponding [[cut-elimination]] theorem.

\hypertarget{LinearAndAffine}{}\subsection*{{Linear (BCI) and affine (BCK) combinatory logic}}\label{LinearAndAffine}

Versions of combinatory logic that correspond to [[linear logic]] and [[affine logic]] have been studied under the names \textbf{BCI logic} and \textbf{BCK logic} respectively, with the letters indicating the combinators used, where

\begin{itemize}%
\item $B = \lambda x.\lambda y.\lambda z. x(yz) : (B\to C) \to (A\to B) \to (A\to C)$
\item $C = \lambda x.\lambda y.\lambda z. (xz)y : (A\to (B\to C)) \to (B \to (A\to C))$

\end{itemize}
The combinator $I$ is also definable as $CKK$, so it is also available in BCK logic (which might therefore be called BCKI logic). Similarly, traditional combinatory logic could be called ``SKI logic'', or just ``SK logic''.

Note that $B$ has the same type as the ``composition'' operation in a [[closed category]], while $C$ has the type of a symmetry/exchange for a closed category. Similarly, $K$ is a sort of [[weakening rule]] while $S$ combines composition, symmetry, and [[contraction rule|contraction]].

\hypertarget{remark}{}\subsection*{{Remark}}\label{remark}

A \emph{partial combinatory algebra} , also called a \emph{Sch\"o{}nfinkel algebra} , is an algebraic structure that abstracts the structure of (partial) combinatory logic. They play an important role in the theory of [[realizability topos|realizability toposes]].

\hypertarget{related_pages}{}\subsection*{{Related pages}}\label{related_pages}

\begin{itemize}%
\item [[partial combinatory algebra]]
\item [[combinator]]
\item [[lambda-calculus]]
\item [[categorial grammar]]

\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item [[Moses Schönfinkel]], \emph{\"U{}ber die Bausteine der mathematischen Logik} , Math. Ann. \textbf{92} (1924) pp.305-316. (\href{http://gdz.sub.uni-goettingen.de/dms/load/img/?PID=GDZPPN002270110}{gdz}) English translation with comments by Quine pp.355-366 in van Heijenoort (ed.), \emph{From Frege to G\"o{}del} , Harvard UP 1967.


\item M. W. Bunder, Category Theory Based on Combinatory Logic , Arch. Math. Logik \textbf{24} (1984) pp.1-15. (\href{http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=GDZPPN002045680}{gdz})


\item [[Peter Freyd]], \emph{Combinators} , Contemp. Math. \textbf{92} (1989) pp.63-66.


\item R. Hindley, J. Seldin, \emph{Introduction to Combinators and $\lambda$-Calculus} , Cambridge UP 1986.


\item [[Jim Lambek]], \emph{Deductive systems and categories III. Cartesian closed categories, intuitionist propositional calculus, and combinatory logic} , pp.57--82 LNM \textbf{274} Springer Heidelberg 1972.



\end{itemize}
[[!redirects combinatory logics]] [[!redirects BCI logic]] [[!redirects BCI-logic]] [[!redirects BCK logic]] [[!redirects BCK-logics]]



\end{document}