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
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
0
votes
0
answers
34
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$ ...
0
votes
1
answer
75
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 ...
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 ...
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 ...
1
vote
1
answer
211
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....
4
votes
1
answer
178
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 $\...
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, $...
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 ...
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 ...
3
votes
1
answer
113
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 ...
0
votes
1
answer
83
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 ...
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 ...