# Questions tagged [lambda-calculus]

For questions on the formal system in mathematical logic for expressing computation using abstract notions of functions and combining them through binding and substitution.

372 questions
23 views

9 views

### Can someone give me a hint on how to solve this lambda calculus related question?

et TRUE = \x y -> x let FALSE = \x y -> y let ITE = \b x y -> b x y let NOT = \b x y -> b y x let AND = \b1 b2 -> ITE b1 b2 FALSE let OR = \b1 b2 -> ITE b1 TRUE b2 -- YOU SHOULD ONLY ...
24 views

12 views

### Partial derivative of a function within a function, lambda calculus

$$L = u_1 (x_1,y_1) + \lambda \left[ u_2(x_2, y_2) - u_0^2 \right] + \mu \left[0 - T(x_1,x_2,y_1,y_2) \right]$$ $\lambda$ and $\mu$ are the multipliers. There's a number of variables to partially ...
159 views

### Theorem on alpha conversion in type free lambda calculus

I am going through Lemma 1.2.11 of "Lectures on the Curry-Howard Isomorphism" by Morten Heine Sørensen and Pawel Urzyczyn. There is a free sample that includes this lemma here: https://play.google.com/...
10k views

52 views

### lambda calculus evaluation

I have a question about lambda calculus. I just read that it doesn't matter in which way expressions get evaluated. So my question is: $(\lambda f.\lambda x.f(fx)) (\lambda y.y+1) 2$ so we can ...
23 views

68 views

### Ambiguity of definition of substitution in lambda calculus

From Type Theory and Formal Proof, An Introduction by Rob Nederpelt and Herman Geuvers: Definition 1.6.1 (Substitution) (1a) $x[x := N] \equiv N$, (1b) $y[x := N] \equiv y$ if $x \not \equiv y$, (...
45 views

### Definition of renaming in lambda calculus

From "Type Theory and Formal Proof, An Introduction" by Rob Nederpelt and Herman Geuvers: Definition 1.5.1 (Renaming; $M^{x \to y}$; $=_{\alpha}$) Let $M^{x \to y}$ denote the result of replacing ...
32 views

### Is there a right identity for Application in Lambda calculus?

Such a function E that: ∀F (F E = F) It's obviously, that the left identity E' (E' F = F) ...
47 views

86 views

### Evaluate this alpha substitution $[(zx)/x] \, \lambda z.xyz$

I am having difficulty with the following problem: Calculate the result of this substitution, renaming the bound variables as needed, so that substitution is defined $[(zx)/x] \, \lambda z.xyz$ ...
66 views

47 views

### (𝜆x. (𝜆y. y)) (𝜆a. (𝜆b.a)) beta reduction

I've came across an example and I'm not quite sure on how the solution was met after performing beta-reduction on the following expression. It doesn't show any of the steps. Any help is appreciated! (...
94 views

### Reducing Lambda to Normal Form

I'm having issues trying to reduce (λx. (λy. y x) (λz. x z)) (λy. y y) to its normal form. I get to ...
35 views

### Function in Lambda Calculus

Yesterday I have been trying to complete this exercise. I have to find: $$((map)l)t \simeq \lambda k \lambda x ((k)(t)t_1)....((k)(t)t_n)x$$ where $$l=\lambda k \lambda x ((k)t_1)....((k)t_n)x$$ ...
68 views

### How to find a simple function in Lambda Calculus?

I was doing this exercise : Find the function $$exchange$$ such that: $$(exchange)t \simeq \lambda p(p)t_2 t_1$$ where $$t= \lambda p(p)t_1 t_2.$$ I found  exchange= \lambda p(p) (\lambda c (S \ \...
41 views

### $(M B) (M B)$ canonical form

Are there lambda terms $M$ and $B$ with $M \neq B$, so that $M B$ and $(M B) (M B)$ have the same canonical form? Is a problem I encountered while I am still new with lambda calculus I approached ...
113 views

### what are the 5 simplest lambda calculus expresions

I'm struggling to learn lambda Calculus. I think what might really help is to see the simplest functions that you can create in lambda calculus and how they might be combined to make more complex ...
I have the following and am asked to evaluate it (I've posted this question elsewhere but I have a new worry with evaluating the function). $[[\lambda f.\lambda m. f(m + m^2))]([\lambda n.2n])](3)$ ...