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

612 questions
Filter by
Sorted by
Tagged with
33 views

### How do I define a notion of infinite coproducts for objects in a category?

As part of a project I'm working on; I am writing an interpreter for the STLC (simply typed $\lambda$-calculus) in which the type-checking algorithm treats isomorphic types as "equal". I ...
110 views

### Reasoning in natural language vs. reasoning in formal language

In ZFC set theory, we first used axioms to prove the existence of the set of natural numbers based on its definition, and after proving uniqueness, we introduced $\mathbb{N}$ in a new symbolic system ...
• 1,748
38 views

So, this would be a definition of False in the Calculus of Constructions: $$\bot = \forall x : \mathbf P . x$$ And, according to Wikipedia, this is an inference rule: $${\Gamma \vdash A : K \qquad \... 0 votes 1 answer 27 views ### Proving that different definitions for the successor function are not \beta-equal in the \lambda-calculus In Lectures on the Curry-Howard Isomorphism, by Sørensen and Urzyczin, it is informed that these two definitions of the successor function over the Church numerals aren't \beta-equal:$$ A_s = \... 134 views

### Unnested universes in type theory

All sources I looked at only talk about a nested family of universes $U_0 : U_1:U_2: \dots$ (for example, the HoTT book, or Notes on Universes in Type Theory, or this answer). If one has two (or more) ...
• 177
1 vote
36 views

• 1,748
238 views

### Is lambda calculus a sub-system of first-order logic and set theory?

I have been reading lambda calculus for a while, and I have always had the question: is lambda calculus a subsystem under first-order logic and set theory? For instance, in many textbooks, we assume ...
• 1,748
1 vote
57 views

### How do we establish the correspondence between the Krivine machine and classical logic?

In this paper, Krivine describes his machine and maps it to classical logic (he implements something like call/cc at the end). Only, I have trouble understanding how he establishes this correspondence ...
• 11
68 views

### Tetration of Church numerals? [closed]

I haven't seen any examples of tetration of Church numerals, so I was trying to do it myself. Tetration is iterated exponention, for example: $2 \uparrow\uparrow 3={2^{2}}^{2}$. Unfortunately, I haven'...
• 1,374
35 views

• 197
12 views

### Coming up with an uncurried function division

Question. Define a $\lambda$-expression $\underline{div}$ with the property that: $$\underline{div} (\underline{m}, \underline{n}) = (\underline{q},\underline{r})$$ where q and r are the quotient ...
• 197
13 views

• 197
37 views

### How to show beta equivalence of property of Y combinator

How to show that $\underline{Y}f =_{\beta} f(\underline{Y}f)$ where $\underline{Y}$ is the usual Y combinator? Thanks.
• 197
38 views

### Why does ($\lambda$c.x) $\lambda$e.f simplify to x?

Why does ($\lambda$c.x) $\lambda$e.f simplify to x? The next step in this reduction I thought was to replace all c's with x. But there are no c's. What happens with the $\lambda$e.f? I have gotten it ...
• 103
1 vote
38 views

• 197
28 views

• 197
38 views

### Prove the existence of $F \in \Lambda$ such that $Fx = xF$ for arbitrary variable $x \in \Lambda$

I recently met the problem as indicated in the title: find an $F \in \Lambda$ such that $Fx = xF$ for arbitrary variable $x \in \Lambda$. I am not only seeking a solution, but also a systematic way to ...
• 1,748
17 views

### Showing that iszero of successor n is false

Intuitively, it seems true that $\underline{iszero}(\underline{suc} \ \underline{n})=\underline{false}$ since $\underline{suc} \ \underline{n}$ is always greater than zero for any natural number $n$ (...
• 197
1 vote
23 views

• 197
16 views

### Evaluating lambda expression to correctly substitute term into body

I want to show that $$ADD = \lambda mn. \lambda f. COMPOSE (mf)(nf)$$ given that $$ADD = \lambda mn. \lambda fx. (mf)((nf)x)$$ where where $m,n$ are Church numerals and $f$ is successor function, ...
• 197
1 vote
87 views

### Resources about Constructive "Extreme" Substructural Logics

Substructural logics can be obtained by dropping different structural rules, most commonly contraction, weakening, exchange. Effects of not having these rules have been studied widely in literature, ...
• 11
24 views

• 197
16 views

### Evaluating substitution to show it is not valid

I'm trying to show that the following is not valid substitution. $$(λy. λy. y) (λy.y) (λz.y) = (λy.y) [ (λy.y) / y] (λz.y)\\= (λy. λy.y) (λz.y) = (λy.y) [ (λz.y) / y] = (λy. λz. y)$$ Since $y$ is ...
• 197
24 views

### Is there a valid application where variables are not distinct and occur free in operand

Consider $$(\lambda V_1..V_n. E)E_1..E_n$$ Is there a case where application of this form is valid if not all $V_i$ are distinct and some $V_i$ occur free in $E_i$? Here's an example where it is not ...
• 197
23 views

### Definition of variable V occurring free in lambda expression E

What does the following mean? $$(\lambda V_1 V_2.E) E_1 E_2$$ "$V_2$ occurs free in $E_1$." Does this mean $E_1$ contains references to $V_2$? Could you explain with examples? Thanks a ...
• 197
20 views

### Prove that if invalid beta conversion is allowed then any two lambda expressions are equal

Here is the question from text: Find an example which shows that if substitutions in $\beta$-reductions are allowed to be invalid, then it follows that any two $\lambda$-expressions are equal. Here is ...
• 197
40 views

### Prove that equality is symmetric in lambda calculus

I want to prove that = is symmetric in lambda calculus. ie. If $E=E'$ then $E'=E$. From text I came across that if for instance $$E_1 \to_\beta E_2 \to_\beta E_3$$...
• 197