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

659 questions
Filter by
Sorted by
Tagged with
38 views

### Set theoretic definition of terms of the untyped lambda calculus

I am trying to translate the following definition (in Agda) of intrinsically scoped terms of the untyped lambda calculus into more mathematical (in particular set theoretical) notation: ...
• 371
1 vote
18 views

• 111
64 views

### Defining the Y combinator in terms of S, K and I

We know that the Y-combinator is defined as: $$\text{Y}:=\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$ Wikipedia says :$$\text{Y}:=\text{S(K(SII))(S(S(KS)K)(K(SII)))}$$ Now the question is: What ...
• 1,204
27 views

### Can a CL-term have multiple fixed points?

Given a CL term $E$, can there exist multiple non-equivalent fixed points for $E$? I think: any fixed point of $E$ can be expressed as $Y(E)$, this expression cannot reduce to multiple non-equivalent ...
• 1,204
47 views

• 1,204
1 vote
57 views

### Is this $\alpha$-conversion correct?

I found this $\alpha$-conversion below in a certain book: $(\lambda x. x(\lambda z. xy)) = \alpha (\lambda z. z(\lambda x. zy))$ Well... this seems wrong to me, since $z$ is a binding variable in ...
• 4,220
89 views

### If closed lambda calculus expression $M$ doesn't have a normal form, can $λx.λy.(M (x y))$ have a normal form?

I'm trying to solve the following problem, but I'm not sure if it's actually possible/true: "Let $M$ be a closed pure lambda term without normal form. Prove that $\lambda x.\lambda y.(M (x y))$ ...
32 views

### Induction on the length of a lambda-term

Let M be a λ -term, with length m, that is: m = lgh(M). Well... I think "induction on lgh(M)" means the same as "finite induction on m". But I'm not sure. I ask for help.
• 4,220
55 views

• 291
1 vote
143 views

### Simplyfing $(\lambda y. z)((\lambda x. x x)(\lambda x. x x))$

I need to simplify this expression. $(\lambda y. z)((\lambda x. x x)(\lambda x. x x))$ However, what's interesting to me are two things: Should I start simplifying $((\lambda x. x x)(\lambda x. x x))$...
• 623
72 views

### How to convert lambda expressions into morphisms in a Cartesian Closed Category?

I'm trying to understand how named variables relate to function composition. So, in a program, it's useful to have named intermediate variables, so you can use them multiple times in the future: ...
• 423
104 views

### Proving that the Curry fixed point combinator y and the Turing fixed point combinator θ cannot be proved equal in λβ

$y = λf.(λx.f(xx))(λx.f(xx))$ $θ = (λxy.y(xxy))(λxy.y(xxy))$ I'm trying to prove that $y \neq \theta$ in λβ. My idea was to assume the contrary, then by Church - Rosser, there exists some $u$ s.t. ...
• 177
Consider this sequence of lambda functions: $\lambda xy. yxy$, $\lambda xyz. zxyz$, $\lambda xyzw. wxyzw$, etc. I would like some lambda function $g$ such that when $g$ is applied to $n$, it returns ...