Combinatory logic

:This article is about a topic in mathematical logic and theoretical computer science, and is not to be confused with combinatorial logic, a topic in electronics.

(I I)

I

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

which means that the normal form of (S I I Z) is simply I, another

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

contradiction. Therefore, the hypothetical normal-form combinator N

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

cannot exist.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Combinatory terms as graphs

(TO DO: Add details with illustrations; don't forget to discuss the effect of

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

fixed-point combinators.)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Applications

Compilation of functional languages

Functional programming languages are often based on the simple but

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

universal semantics of the lambda calculus. (Add details.)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

David Turner used his combinators to implement the SASL language.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

(Discuss strict vs. lazy evaluation semantics. Note implications of

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

graph reduction implementation for lazy evaluation. Point out

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

efficiency problem in lazy semantics: Repeated evaluation of the same

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

expression, in, e.g. (square COMPLICATED) => (* COMPLICATED

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

COMPLICATED), normally avoided by eager evaluation and call-by-value.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Discuss benefit of graph reduction in this case: when (square

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

COMPLICATED) is evaluated, the representation of COMPLICATED can be

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

shared by both branches of the resulting graph for (* COMPLICATED

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

COMPLICATED), and evaluated only once.)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Logic

The Curry-Howard isomorphism implies a relationship between logic

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

and programming: Every valid proof of a theorem of logic corresponds

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

directly to a reduction of a lambda term, and vice versa. Theorems

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

themselves are identified with function type signatures. Specifically, typed combinatory logics

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

correspond to Hilbert systems in proof theory.

Related Topics:
Hilbert system - Proof theory

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

(Add: Demonstration that the axioms

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

(a -> a)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

(a -> b -> a)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

(a -> b -> c) -> (a -> b) -> (a -> c)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

are complete for the intuitionistic fragment of propositional logic.)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

See also:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• graph reduction machine
• supercombinators

References

• "Über die Bausteine der mathematischen Logik", Moses Schönfinkel, 1924, translated as "On the Building Blocks of Mathematical Logic" in From Frege to Gödel: a source book in mathematical logic, 1879-1931, ed. Jean van Heijenoort, Harvard University Press, 1977. ISBN 0674324498 The original publication of combinatory logic.
• Combinatory Logic. Curry, Haskell B. et al., North-Holland, 1972. ISBN 0720422086 A comprehensive overview of combinatory logic, including a historical sketch.
• Functional Programming. Field, Anthony J. and Peter G. Harrison. Addison-Wesley, 1998. ISBN 0201192497
• "Foundations of Functional Programming". Lawrence C. Paulson. University of Cambridge, 1995.
• "Lectures on the Curry-Howard Isomorphism". Sørensen, Morten Heine B. and Pawel Urzyczyn. University of Copenhagen and University of Warsaw, 1999.
• 1920-1931 Curry's block notes
• "Principal Type-Schemes and Condensed Detachment", Hindley and Meredith, Journal of Symbolic Logic (JSL), Volume 55 (1990), Number 1, pages 90-105