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.
676 questions
3 votes
1 answer
97 views
Compactness through Scott topology on the poset of open subsets
Definitions: Let $\Gamma$ be a topological space and $\mathcal O(\Gamma)$ the poset of open subsets of $\Gamma$. We say a subset $X \subseteq \mathcal O(\Gamma)$ is directed if for all $A,B\in X$ ...
- 1,768
0 votes
1 answer
77 views
How to Read “A Set of Postulates for the Foundation of Logic” by Church
In particular , the first place I feel really lost is with his statement of some basic logical operators as definitions. For example, equality: $\lambda u \lambda v . P(u, v) . P(v, u)$ Where P is ...
- 17
4 votes
1 answer
139 views
A "gcd" of two lambda terms [closed]
Let $M, N, P, Q$ be pure untyped lambda terms. Suppose that $M \stackrel{*}\rightarrow P, Q$ and $N \stackrel{*}\rightarrow P, Q,$ where $\stackrel{*}\rightarrow$ denotes that the term on the left can ...
- 100
2 votes
0 answers
51 views
Errata in "Lambda-Calculus and Combinators, an Introduction" [closed]
I'm studying the book Lambda-Calculus and Combinators, an Introduction by J. Roger Hindley and Jonathan P. Seldin. I believe there is a typographic error in their theorem 1.41, which I'll detail below....
2 votes
1 answer
141 views
Application vs composition in lambda calculus & an explanation for certain conventions
Application in lambda calculus produces a lambda term $(MN)$ from two other lambda terms $M$ and $N$. According to wikipedia this may be thought of as applying a function to an argument. I have two ...
- 21.3k
1 vote
1 answer
212 views
Confusion about the factorial function in lambda calculus
In this reddit post it is given that $$\text{FAC}=λn.λf.n(λf.λn.n(f(λf.λx.n f(f x))))(λx.f)(λx.x)$$ However when I applied it to $1$ I get: $$\begin{align}\text{FAC}\ 1 &=(λn.λf.n(λf.λn.n(f(λf.λx....
- 9,770
4 votes
1 answer
179 views
Dependent type theory and free variables
I have some doubts regarding my understanding and I hope someone can affirm or negate my guesswork. In untyped and simply-typed $\lambda$-calculus, unless noted otherwise, we consider terms up to $\...
- 305
0 votes
1 answer
61 views
What is the inverse of a beta-reduction? [closed]
I am working through a textbook on type theory and I came across a proof of a statement on $\beta-$equality that I don't understand. It states as follows: $$(\lambda y. yv)z =_{\beta} (\lambda x. zx)v$...
2 votes
1 answer
76 views
Lambda calculus, $M$ does (doesn't) have a normal form. Find $MI$ that doesn't (does) have a normal form. [closed]
I'm trying to construct terms $M_1$, $M_2$ such that $M_1$ has a normal form, but $M_1I$ doesn't. $M_2$ doesn't have a normal form, but $M_2I$ does. This is somewhat related to these two questions, $...
- 125
1 vote
1 answer
94 views
Lambda-calculus expression for iterated application of a function
I am trying to construct a lambda expression which works in the following way: assume you have a function $f$ and an argument $x$. The lambda expression I'm trying to build is of the form $P f x$ and ...
- 291
0 votes
1 answer
84 views
Free variables preserved in beta-reduction, lambda calculus
In a previous post, it was stated that “If $M$, $N$ are $\lambda$-terms, and $M \twoheadrightarrow_{\beta\eta} N$, then $fv(N) \subseteq fv(M)$.” Do you have a reference for this statement? I cannot ...
- 11
3 votes
1 answer
115 views
Existence of a Pre-Term in $\lambda$-Calculus where Substitution is Defined.
I am reading Lectures on the Curry-Howard Isomorphism by Sorensen and Urzyczyn, and I got stuck when trying to fill in the details of Lemma 1.2.12(2). Below is the statement of Lemma 1.2.12. Lemma 1.2....
1 vote
1 answer
202 views
"Mechanism of Substitution" captured by λ-calculus
I am reading Type Theory and Formal Proof: An Introduction by Nederpelt and Geuvers. In the Foreword, there is the following, which I quote: Frege did not get far ...
- 421
0 votes
1 answer
84 views
Confluence and beta-reduction
I am studying lambda calculus at university and I came across beta-reduction. I don't know if I don't understand confluence, and beta-reduction, but the term (𝜆x.𝜆y.x)(𝜆z.z)(𝜆w.w) seem to give ...
- 13
1 vote
1 answer
92 views
Böhm's theorem for more than two terms
Böhm's theorem says that for two distinct normal lambda terms $A$ and $B$, and two arbitrary terms $U$ and $V$, there exists a term $X$ such that $XA=U$ and $XB=V$. One obvious extension is increasing ...
- 11