New answers tagged lambda-calculus
4
Generally speaking, in algebra, a congruence relation is an equivalence relation such that operations on equivalent objects yield equivalent objects. In the lambda calculus, a congruence is an equivalence relation such that constructing terms from equivalent terms yields equivalent terms: if $M \equiv M'$ and $N \equiv N'$ then $M\,N \equiv M\,N'$, and if $M ...
answered yesterday
Gilles 'SO- stop being evil'
39.8k7 gold badges105 silver badges170 bronze badges
1
"Congruence" in the context of lambda calculus is usually "alpha-congruence". "alpha-congruent" means "differring only if at all in the names of bound variables".
For instance, $\lambda x. x \equiv_\alpha \lambda y.y$ and $\lambda xy.x(xy) \equiv_\alpha \lambda yx.y(yx)$ (bound variables $x$ and $y$ were swapped), but $...
3
First, let us show that the two assumptions are necessary. Here is an example showing what goes wrong when $x = y$. Take $t = x$, $u = 1$, $v = 2$. We have
$$
x\{x := 1\}\{x := 2\} = 1\{x := 2\} = 1,
$$
whereas
$$
x\{x := 2\}\{x := 1\{x := 2\}\} =
2\{x := 1\} = 2.
$$
Next, here is an example showing what goes wrong when $x$ is not free in $v$. Take $t = y$, $...
0
One standard way to prove that a language is Turing-complete is to implement a simulator for a Turing machine (or for any other Turing-complete language) in that language. That is typically straightforward but boring, for most general-purpose languages.
You can find more resources on Turing-completeness in turing-completeness; see especially, e.g., Is there ...
1
You are looking for Church encodings of datastructures in $\lambda$-calculus, and in particular of lists.
1
$[3,2,1]$ is just syntactic sugar for $\mathsf{cons} \, 3 \, (\mathsf{cons} \, 2 \, (\mathsf{cons} \, 1 \, \mathsf{nil}))$. $[3,2,1]$ is $\mathsf{cons} \, 3 \, [2,1]$ by definition of the $[\ldots]$ notation.
Because $\mathsf{cons}$ is part of the definition of lists, it isn't meaningful to ask whether $\mathsf{cons}$ is correct on its own. The meaningful ...
answered Dec 24 '20 at 17:30
Gilles 'SO- stop being evil'
39.8k7 gold badges105 silver badges170 bronze badges
Top 50 recent answers are included
