51

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 one where not all statements can be proved. In classical logic, this is equivalent to the absence of a contradiction, i.e. a theory is inconsistent if and only ...


30

I haven't read this anywhere, but this is how I believe $Y$ could have been derived: Let's have a recursive function $f$, perhaps a factorial or anything else like that. Informally, we define $f$ as pseudo-lambda term where $f$ occurs in its own definition: $$f = \ldots f \ldots f \ldots $$ First, we realize that the recursive call can be factored out as ...


21

The original Curry-Howard correspondence is an isomorphism between intuitionistic propositional logic and the simply-typed lambda calculus. There are, of course, other Curry-Howard-like isomorphisms; Phil Wadler famously pointed out that the double-barrelled name "Curry-Howard" predicts other double-barrelled names like "Hindley-Milner" and "Girard-Reynolds"...


14

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 represented by the tree @ / \ / \ @ K2 / \ / \ S @ / \ / \ S S To each tree $T$ associate its ...


11

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 there have to be a "real-world application"? Turing machines, for example, are hardly ever used "in the real world" but they form the basis of the theory of ...


11

As Yuval has pointed out there is not just one fixed-point operator. There are many of them. In other words, the equation for fixed-point theorem do not have a single answer. So you can't derive the operator from them. It is like asking how people derive $(x,y)=(0,0)$ as a solution for $x=y$. They don't! The equation doesn't have a unique solution. Just ...


11

Quick note, I allow parametric polymorphism (System F) in this system so that S, K and I can work over all types. Notice that without pattern matching, we can't write an if no matter what we do. We have absolutely no operations on booleans. There is no way to distinguish True from False. Instead try true : a -> a -> a true = \t -> \f -> t ...


9

The Curry-Howard relates type systems to logical deduction systems. Among other things, it maps: programs to proofs program evaluation to transformations on proofs inhabited types to true propositions type systems to logical deduction systems If the type system admits a Y combinator, then that means that the corresponding logical deduction system is ...


8

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 an open term. The programming language equivalent of an open term would be an expression referring to a variable that's simply not in scope. Not just not in ...


7

The equivalence is just equivalence in the equational $\lambda$-theory under discussion. In this case, it's the theory outlined in Table 1. Note that this theory does not include $\eta$: doing so would make the theory extensional, and the point is eventually that $\xi$ respects $\lambda$'s intensionality, while it would make CL partially extensional. I am ...


6

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 $f,g$. Thus, $F,G$ are Scott-continuous functions. Then, we have that the semantics of $Y(f \circ g)$ is, according to the Kleene's fixed point theorem $$ (1) =...


6

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, $\lambda x.\lambda y.x$ has type $a \to (b \to a)$ (where $a \to b$ means "function from $a$ to $b$"), which corresponds to the logical statement $a \implies (b \...


6

Intuitively speaking, a non-terminating program needs either: a combinator such as $Y$ which, when applied, reduces to a larger expression containing itself; or two combinators such as $S$ which, when applied, replicate at least one of their arguments: one to do the initial replication and one to be replicated. Unlambda lacks a combinator of the first type,...


6

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 Barendregts' The Lambda Calculus, Its Syntax and Semantics (aka "the bible"). Corollary 20.3.3: The function $\delta:L'^2\to L'$, defined by $$ \delta(M, N) = \...


6

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}{\mathbf{(}} (\lambda x.f(xx))) (\lambda x.f(xx)) \color{red}{\mathbf{)}}$$ Beware that different authors use different conventions for parentheses. But under ...


6

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 in some OCaml libraries as well (see here). According to wikipedia, people call this function (or combinator) $C$ in the context of combinatory logic (that name ...


5

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 well known combinators), while $P,Q,R$ range over all the possible $CL$ terms (built from $K,S$, variables and application). The relation $=$ is postulated to ...


5

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 (a \rightarrow b) \rightarrow a \rightarrow c \\ a \rightarrow (b \rightarrow a) \end{array} $$ The first time I saw these axioms, I wondered why on earth ...


5

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 A = K$ and $\Gamma B = S$. You don't get to constrain $\Gamma = A$ or the required form $\lambda x. x U V$. There may be a way to use Böhm's theorem on a ...


5

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 not contain an ill-typed subterm). If there's no objection, I won't delete it, since it presents a very productive proof technique for the typed setting. Recall ...


4

not an expert on this but here are two historical papers that seem to be closely relevant to the question and it is possibly a semi active area of research. Turner proposed a set of combinators that can be reduced to SK combinators. this next paper argues that Turner combinators even not reduced to SK combinators leads to exponential blowup (and that ...


4

This isn't probably a standard name, but in The Implementation of Functional Programming Languages in Section 16.2.4 Simon Peyton Jones calls it S'. It is defined as an optimization combinator S (B x y) z = S' x y z The following example is from the mentioned section. Consider λx_n...λx_1.PQ where P and Q are complicated expression that both use all the ...


3

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 an application $(UV)$ needs to be addressed; we certainly would like to get $[x].([y].([z].xz(yz)))$ converted into its corresponding combinator $\mathsf{S}$. ...


3

So you need to define a fixed point combinator fix f = f (fix f) = f (f (fix f)) = f (f (f ... )) but without explicit recursion. Let's start with the simplest irreducible combinator omega = (\x. x x) (\x. x x) = (\x. x x) (\x. x x) = ... The x in the first lambda is repeatedly substituted by the second lambda. Simple alpha-...


3

EDIT This answer is incorrect, as the other answerer correctly pointed out. I used the translation into combinatory logic from Asperti & Longo, which is subtly different from the one in Selinger. In fact, this illustrates a crucial point: "the combinatory interpretation" of lambda calculus is not a single thing! Different authors do it slightly ...


3

The axiom scheme you reference represents a classical logic, i.e. one with excluded middle. The computational interpretation of Peirce's law (implicitly embodied in Łukasiewicz's system) is call/cc. Neither iota nor jot support first-class continuations (or continuations of any sort), so they do not encode or imply Peirce's law. Added much later: I think ...


2

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 sophisticated example would be Linq2SQL (the SQL Server implementation) which efficiently performs complex transformations that segregate the portions of the ...


2

A common encoding used for such tasks is Base64. It is easy to implement and it has been implemented multiple times in many main-stream languages. However, it is not exactly suited for being read by humans. The basic underlying idea is that a character of Latin alphabet is encoded in ASCII using 6 bits. The encoding alphabet is completed by few punctuation ...


2

Yes, fixed point combinators are sufficient for general recursion and Turing complete computations. In my Awelon project languages, fixed point combinators are the only way to model recursion. In practice, working directly with fixed point is rather annoying. However, it isn't difficult to build more conventional loop primitives (while, until, repeat) and ...


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