New answers tagged

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 ...


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 ...


Top 50 recent answers are included