Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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.

2
votes
2answers
609 views

Meaning of variables and applications in lambda calculus

The wikipedia definition of lambda terms is: The following three rules give an inductive definition that can be applied to build all syntactically valid lambda terms: a variable, $x$, is ...
6
votes
2answers
124 views

Problem with a basic lemma in Lambda Calculus

I have some serious problems with Lambda Calculus. In an introduction by Barendregt and Barendsen at page 11 there is the following lemma, whose proof I do not completely get. $\mathbf{\lambda} \...
0
votes
1answer
159 views

How to prove Y Y = Y (Y(Y))

I found a prove online, but I can not fully understand it. The prove is like this: let Y = lambda y . (lambda x . y (x x)) (lambda x . y (x x)) ...
114
votes
9answers
26k views

Learning Lambda Calculus

What are some good online/free resources (tutorials, guides, exercises, and the like) for learning Lambda Calculus? Specifically, I am interested in the following areas: Untyped lambda calculus ...
23
votes
2answers
9k views

What's the point of eta-conversion in lambda calculus?

I think I'm not understanding it, but eta-conversion looks to me as a beta-conversion that does nothing, a special case of beta-conversion where the result is just the term in the lambda abstraction ...
9
votes
1answer
787 views

Proving that $\Omega = (\lambda x.xx)(\lambda x.xx)$ is not typable in the simply typed lambda calculus

I am trying to prove that $\Omega = (\lambda x.xx)(\lambda x.xx)$ is not typable in the simply typed lambda calculus. Surprisingly, different textbooks and lecture notes do not contain that proof, ...
10
votes
2answers
553 views

What is the shortest function of lambda calculus that generates all functions of lambda calculus?

I suspect there's a good chance the answer to this is unknown and hard (or at least extremely tedious), but I figured it would be worth asking. It's well known that the functions $K:=\lambda x.\...
6
votes
1answer
593 views

Fixed point combinator (Y) and fixed point equation

In Hindley (Lambda-Calculus and Combinators, an Introduction), Corollary 3.3.1 to the fixed-point theorem states: In $\lambda$ and CL: for every $Z$ and $n \ge 0$ the equation $$xy_1..y_n = Z$$ can ...
5
votes
2answers
941 views

Understanding η-conversion (Lambda Calculus)

Let $h \in A\rightarrow (B\rightarrow C)$ I'm trying to understand the following reduction: $$\lambda x\in A. \lambda y \in B.(h(x))(y) \\= \lambda x\in A.h(x) \\= h$$ Apparently, this is done by ...
2
votes
1answer
308 views

I did not understand one thing in the proof of substitution lemma?

The substitution lemma in lambda-calculus is proved by the following way, but I just did not understand the application of induction hypothesis in it. The lemma as shown below, where $x$ and $y$ are ...
0
votes
1answer
151 views

Actually defining functions in Church's simple type theory

I've been reading up on Church's simple type theory and much of the concepts make sense to me. However, I can't actually figure out how to define functions explicitly using the notation provided. ...
0
votes
1answer
115 views

Lambda calculus: How to define a function that simulates $\neg p\vee q$?

I am making my first steps in lambda calculus, so please bear with me. I want to create a lambda function, that given two boolean expressions (either $F$ or $T$ - defined below), simulates the formula ...
3
votes
0answers
149 views

What is the desirable function identification when setting up arrows in the category of types?

My question is which functions can not be allowed in a statically typed programming language, so that the "canonical" category is less coarse than what you get if you define it's arrows to be ...
2
votes
2answers
836 views

How do scoping rules work in the Lambda Calculus with nested functions

Let's say I have a lambda expression like this: $$(\lambda a . (ab))(c)$$ It reduces to $$cb$$ But let's say I have a nested function $$(\lambda a . (\lambda x.(ax)))(b)$$ Does this reduce to $$...
2
votes
1answer
216 views

Simple type theory: Proof inexistance of closed term

In simple type theory, how can I prove that there is no closed term of type? $$((P \Rightarrow Q) \Rightarrow Q) \Rightarrow P$$
2
votes
1answer
64 views

$\lambda$ calculus how encode A $\leftrightarrow$ B

I am spending days figuring out how can i show A $\leftrightarrow$ B such that A=B=True or A=B=False as $\lambda$ calculus I know that we can show : True ≡ λxy.x False ≡ λxy.y and ≡ λpq. p q ...
2
votes
2answers
784 views

Self-application in Church's untyped lambda calculus

In "Proposition as Types" by Philip Wadler mentions the weaknesses of untyped lambda calculus and "Russell's logic" concerning self-application. Whereas self-application in Russell’s logic leads to ...
1
vote
1answer
216 views

Lambda calculus typing

I'm trying to find a type T such that I can create a derivation tree for the following expression: λx.λy.((xy)y) : T Am I right in thinking that there is no such T for this to be possible? If I'm ...
1
vote
1answer
56 views

Lambda-calculus - Basic Problem with application of Fixedpoint theorem

This question is a sort of follow-up of a previous one. Again, I just do not really see how the $\lambda$-calculus actually works. Now, the problem is with Example 2.13 at page 12 of Introduction to ...
1
vote
1answer
88 views

Lambda calculus expression reduction

I don't know the correct answer how this reduction should've be done. Should I simply put λfx.fx in a place of m and λzy.zzy in a place of n? ...
1
vote
1answer
54 views

Trouble Replicating Proof of a Lambda Calculus Fixed Point Theorem Corollary

From pg. 35 of Lambda Calculus and Combinators An Introduction: Corollary 3.3.1 in $\lambda$ and $CL$: for every $Z$ and $n \ge 0$, the equation $$ xy_1 \ldots y_n = Z $$ can be solved ...
0
votes
1answer
155 views

The definition of the factorial using continuations in the Lambda calculus

I am trying to understand why the definition below of the factorial given here is an example of a continuation: https://www.seas.harvard.edu/courses/cs152/2010sp/lectures/lec11.pdf $$FACT_{cps} = Y \...
0
votes
1answer
538 views

Identifying All Redexes in Lambda Expression

I am self-studying Lambda calculus and have encountered a question where I need to identify all the redexes of the following expression: ...
0
votes
1answer
274 views

$\lambda$-calculus: structural induction principle over $\Lambda$

The set $\Lambda$ is given inductively by: $x\in\Lambda$, if $x$ is a variable; $(\lambda x M)$, if $x$ is a variable and $M\in\Lambda$; $(MN)$, if both $M,N\in\Lambda$. Now, consider the structural ...