# Tag Info

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