New answers tagged lambda-calculus
5
If we keep reducing the right subterm, then yes, we will never get to $v$. But noone says that we are restricted to this decision. The Church-Rosser theorem does not claim that any possible reduction series must lead to $N_3$. Church-Rosser just states that $N_2 \twoheadrightarrow_\beta N_3$, i.e. that there exists some beta reduction series that will lead ...
4
Those features are almost never implemented like the lambda calculus in modern programming language implementation. In some cases, using the lambda calculus representation for datatypes has performance improvements (this is associated with so-called tagless representations). Historically, the Haskell compiler did use this representation early on, but has ...
2
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 context.
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 ...
Top 50 recent answers are included
