Skip to main content
53 votes
Accepted

How does the Y combinator exemplify "Lambda calculus inconsistency"?

It's inspired from real events, but the way it's stated is barely recognizable and “should be regarded with suspicion” is nonsense. Consistency has a precise meaning in logic: a consistent theory is ...
Gilles 'SO- stop being evil''s user avatar
18 votes
Accepted

Is the SK2 calculus a complete basis, where K2 is the flipped K combinator?

Consider the terms of the $S,K_2,I$ calculus as trees (with binary nodes representing applications, and $S, K_2$ leaves representing the combinators. For example, the term $S(SS)K_2$ would be ...
Z. A. K.'s user avatar
  • 355
11 votes

What is the purpose of the SKI combinator calculus(or even lambda calculus)? What are some real life examples of its use?

The obvious application of the lambda calculus is any functional programming language (e.g., Lisp, ML, Haskell), and any language that supports anonymous functions. As for combinator calculus, does ...
David Richerby's user avatar
8 votes
Accepted

Why are combinators important in lambda calculus?

The word "combinator" has some connotations that you don't seem to be intending here and sometimes a stricter definition. Another term for the definition you gave is a closed term. The opposite is ...
Derek Elkins left SE's user avatar
8 votes

How does the Y combinator exemplify "Lambda calculus inconsistency"?

I'd like to add one to what @Giles said. The Curry-Howard correspondence makes a parallel between $\lambda$-terms (more specifically, the types of $\lambda$-terms) and proof systems. For example, $\...
Noncontextual Spelling's user avatar
8 votes

What benefits are obtained by allowing the occurrence of free variables and open terms in lambda calculus?

A subterm of a closed term is not necessarily a closed term. A calculus of closed terms would have to model open terms as well anyway. Pretty much any definition on terms relies on induction over the ...
Gilles 'SO- stop being evil''s user avatar
7 votes

What functions can combinator calculus expressions compute?

To get the ball rolling, and in hopes of other people giving deeper and more detailed answers on the structure of the $\lambda$-definable functions $L'\to L'$, let me cite Corollary 20.3.3 from ...
cody's user avatar
  • 8,233
6 votes

Reduction of the Y combinator

You've misread the definition of $Y$. $(\lambda x.f(xx))) (\lambda x.f(xx))$ is the body of the function. You can put an additional pair of parentheses in the definition: $$ Y = \lambda f. \color{red}{...
Gilles 'SO- stop being evil''s user avatar
6 votes
Accepted

What is the name of the operator that translates from $X\rightarrow(Y\rightarrow Z)$ to $Y\rightarrow(X\rightarrow Z)$?

The function $$\lambda f.\lambda x.\lambda y.f\;y\;x$$ of type $$\forall X. \forall Y. \forall Z.(X \to Y \to Z) \to Y \to X \to Z$$ is often called flip. This is the case in Haskell (see here), and ...
Rodolphe Lepigre's user avatar
6 votes

Is the SK2 calculus a complete basis, where K2 is the flipped K combinator?

EDIT: As the comments point out, this is only a partial answer, since it applies only to the simply-typed $S,K_2,I$ calculus (or rather, it shows that there is no possible definition of K that does ...
Z. A. K.'s user avatar
  • 355
6 votes
Accepted

Y combinator, function composition

It depends on the notion of equivalence you are using. Suppose we compare these terms according to their denotational semantics, on $\omega$-CPO domains. Denote with $F,G$ the semantics of the terms $...
chi's user avatar
  • 14.6k
5 votes

Combinator equivalent to eta conversion

From the Barendregt lambda calculus book, we can find theory $CL$ (combinatory logic) defined as follows $$ K P Q = P \qquad S P Q R = P R (Q R) $$ where $K,S$ are constant symbols (for the ...
chi's user avatar
  • 14.6k
5 votes

What is the purpose of the SKI combinator calculus(or even lambda calculus)? What are some real life examples of its use?

I found SKI useful to understand some logical axioms. For instance, a Hilbert-style axiomatization of (intuitionistic) implication is $$ \begin{array}{l} (a \rightarrow b \rightarrow c) \rightarrow (...
chi's user avatar
  • 14.6k
5 votes
Accepted

Find a lambda term satisfying two equations

This is not directly a consequence of Böhm's theorem. Böhm's theorem states that for any strongly normalizing $A$ and $B$ that are not $\beta\eta$-convertible, there exists $\Gamma$ such that $\Gamma ...
Gilles 'SO- stop being evil''s user avatar
5 votes

Why do combinators look this way?

The combinators $K$ and $S$ first appear in Moses Schönfinkel, Über die Bausteine der mathematischen Logik, though he calls them $C$ and $S$. He actually defines five combinators, $I,C,T,Z,S$, and ...
Yuval Filmus's user avatar
4 votes

Beta reduction of S combinator in pure lambda calculus

Parentheses matter. Honestly, if you are unclear about how $\lambda$-calculus works, it is going to be rather hard to implement it. Here is an explicit counter-example: $$(K S)(K S) = S$$ but $$K S K ...
Andrej Bauer's user avatar
  • 30.9k
3 votes

Understanding A Recursive Definition of CL-Terms in Combinatory Logic

Here are some considerations that could have been used to sort of "derive" the (f) rule: it is natural to define our type of conversion recursively; the general case when the body of "$\lambda$" is ...
Anton Trunov's user avatar
  • 3,479
3 votes

Clear, intuitive derivation of the fixed-point combinator (Y combinator)?

You may have seen the classic example of an equation without a normal form: $$(\lambda x.xx)(\lambda x.xx) \triangleright (\lambda x.xx)(\lambda x.xx)$$ A similar equation is suggested by that for ...
DanielV's user avatar
  • 516
3 votes
Accepted

How, if possible, can we efficiently compute with lazy data structures in 𝜆-calculus?

Although Haskell of course has native recursion, we can ignore it and implement the Y combinator $λf. (λx. f (x x)) (λx. f (x x))$ literally, using a newtype to get ...
Anders Kaseorg's user avatar
3 votes

Why do combinators look this way?

This is so because $K$ and $S$ can be used to generate all other $\lambda$-terms (up to extensional equality), refer to this proof for the details.
Andrej Bauer's user avatar
  • 30.9k
2 votes

Basis sets for combinator calculus

Any set of combinators that contains a cancellative combinator (like K), a composing combinator (like B), a permuting combinator (like C), a duplicative combinator (like W) and the identity combinator ...
baronbrixius's user avatar
2 votes

Basis sets for combinator calculus

It's easy to make other bases by switching out the combinators from one basis with ones that do something similar. For example, starting with BCKW, you can switch $C$ for $T = (\lambda x y. y x)$ (...
Joseph Sible-Reinstate Monica's user avatar
2 votes

Clear, intuitive derivation of the fixed-point combinator (Y combinator)?

Instead of starting with the properties of $\mathrm{Y}$, start with a term that explicitly refers to itself: $$\textbf{letrec }f = \ldots f \ldots f \ldots \textbf{ in } f$$ and consider how it could ...
benrg's user avatar
  • 2,157
2 votes

What is the purpose of the SKI combinator calculus(or even lambda calculus)? What are some real life examples of its use?

Have a look at Microsoft's LINQ (Language INtegrated Query). It makes extensive and quite direct use of lambda calculus to manipulate and transform expression trees. Probably the most complete and ...
Peter Wone's user avatar
2 votes

Why are combinators important in lambda calculus?

A combinator is a lambda expression with no free variables. So, λx.x is a combinator but λx.y is not a combinator. Consider the following: (λxy.xy)(λx.y) = (λy.xy)[x := λx.y] = (λy.(λx.y)y) Notice ...
Dwayne Crooks's user avatar
2 votes

What is the name of the operator that translates from $X\rightarrow(Y\rightarrow Z)$ to $Y\rightarrow(X\rightarrow Z)$?

Given the tag combinatory-logic, the answer in combinatory logic is C, i.e. "the C combinator". Obviously, this name is not self-documenting or going to be obvious in even a slightly more general ...
Derek Elkins left SE's user avatar
2 votes
Accepted

Coding max as an interaction net

Rules for agents in interaction nets are defined by what the principal port of that agent is connected to and each agent has exactly one principal port. In the "max" example, for the top ...
marc's user avatar
  • 56
2 votes

Combinational logic check if bits is prime

Of course, the circuit will just grow rapidly. For 8 bits there is no problem. You check whether bit 0 is 0 or 1. If it is 0, then you check whether the input is 2. If it is 1, then you check bit 7. ...
gnasher729's user avatar
  • 30.5k

Only top scored, non community-wiki answers of a minimum length are eligible