New answers tagged lambda-calculus
0
Try this.... It should help build up the intuition step by step
http://pages.cs.wisc.edu/~horwitz/CS704-NOTES/2.LAMBDA-CALCULUS-PART2.html
Alternatively since it's not really clear what you mean, maybe an example of what kind of abstraction you want for something simpler than sum?
1
The thing to notice here is that your function sum is defined on lists, which are inductively defined. Theoretically, the inductive definition of a list defines for every type T a term
match_list :: T -> (a -> [a] -> T) -> ([a] -> T)
satisfying the property
match_list s t [] = s
match_list s t (x::xs) = (t x xs)
in addition, defining a ...
2
One way to not mess up with variable names in $\lambda$-calculus is to use De Brujin indexes. With this, $\alpha$-equivallence becomes a really obvious syntactic equality, for instance:
\begin{align*}
\lambda x.x &\rightarrow \lambda.0 \\
\lambda z.z &\rightarrow \lambda.0 \\
\lambda x .\lambda y. x &\rightarrow \lambda.\lambda.1 \\
\end{align*}
...
0
If I inline (u => (f)(n => u(u)(n))) into (u => u(u)) I get:
(u => f(n => u(u)(n)))
(u => f(n => u(u)(n)))
Which is exactly the Z-Combinator.
From wikipedia:
let Z = f =>
(u => f(v => u(u)(v)))
(u => f(v => u(u)(v)))
My derivation:
let fix = f =>
(u => f(n => u(u)(n)))
(u => f(n => u(u)(n))...
0
The other answers are good, I just wanted to make it explicit that currying for dependent types is
$$
\textstyle
\prod (x : A) . \prod (y : B(x)) . C(x, y)
\ \cong \
\prod (p : \sum (x : A) . B(x)) . C(\pi_1(p), \pi_2(p))
$$
which is more suggestive in Agda-style notation:
$$
(x : A) \to (y : B(x)) \to C(x,y)
\ \cong\
(p : (x : A) \times B(x)) \to C(\pi_1(...
2
Here is one example:
(λx.(λx.x(λy.x)x)x)x
And by applying alpha equivalnce I can rewrite it to:
(λw.(λz.w(λy.z)z)w)x
Is my understanding correct ?
There is a small error in your rewriting: at λz.w you have changed the meaning of the expression, because now the bound variable refers to the outer lambda abstraction, instead of the inner lambda abstraction ...
Top 50 recent answers are included
