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
0
votes
0
answers
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 ...
4
votes
1
answer
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
0
votes
0
answers
38
views
Why is this proof of False in the Calculus of Constructions not valid?
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 = \...
user1045405
3
votes
2
answers
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
1
answer
36
views
Equivalence of "compatible relation" definitions
$\newcommand{\abstraction}[2]{\lambda #1. #2}$
$\newcommand{\application}[2]{\left(#1 #2\right)}$
$\newcommand{\substitution}[3]{#1 \left[#2 := #3\right]}$
$\newcommand{\freevars}[1]{\operatorname{FV}\...
- 21
0
votes
1
answer
23
views
Can in polymorphic lambda calculus two terms have identical normal forms if we assume that set of their possible types does not intersect?
Let us assume, that we have context $\Gamma$ and two terms $M_1$ and $M_2$ in polymorphic lambda calculus. Let us also assume, that intersection of their possible types in context $\Gamma$ is empty(we ...
1
vote
1
answer
69
views
Lambda Calculus: Proving exponent property by induction
Recently I have learned that given Church numerals $\bar n = \lambda fx.f^n x$ and $\bar m = \lambda fx.f^m x$, we can calculate $\overline{m^n}$ by applying $\exp=\lambda mn.nm$. I believe this means ...
- 23
2
votes
1
answer
48
views
How to prove $M = N$ is equivalent to $M =_{\beta} N$ in Lambda Calculus
Lambda calculus is equipped with a primitive $=$ with the following definition:
(1) For any variable $x$ and lambda term $M, N$, $\left(\lambda x. M\right) N = M\left[x := N\right]$;
(2) For any term $...
- 1,748
3
votes
2
answers
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
0
answers
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
-1
votes
1
answer
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
0
votes
0
answers
35
views
Subterms of a lambda application?
In a book on Type theory I am working through, there is a definition for subterms where the third case covers lambda abstractions and is given by
$$Sub((\lambda x. M)) = Sub(M) \cup \{(\lambda x. M)\}$...
- 1,374
1
vote
0
answers
77
views
Construction of Factorial as a Recursive Function from Initial Functions and Closure Operations
$\newcommand{\domain}[1]{\operatorname{dom} #1}$
Recursive functions have been a topic of importance in computer science. In lambda calculus, the class of recursive functions, $\mathcal{R}$, is ...
- 1,748
2
votes
0
answers
61
views
Show that subtraction is primitive recursive
I want to show that subtraction is primitive recursive: $subtract(x,y)=x-y$.
To do this, I must first show that pred function: $pred(x)=x-1$ is also primitive recursive.
So, let's do that!
First, we ...
- 197
1
vote
1
answer
20
views
How is KMI an application and not abstraction with MI in body in lambda calculus?
Let $K = \lambda zy.z$ (kestrel), $M = \lambda f.ff$ (mockingbird), $I = \lambda x.x$ (identity).
Now I believe $M$, I should be subsumed inside $K$'s function body but my lecture notes say that $K M ...
- 31
0
votes
1
answer
36
views
Showing a function that behaves like pred to be primitive recursive
Let's define $M$ such that for $x \ge 0$:
$$
M(0)=0
$$
$$
M(x+1)=x
$$
Now, I want to show that $M$ is primitive recursive. How should I go about doing this?
Thanks a bunch!
- 197
0
votes
0
answers
20
views
Prove that exponent is primitive recursive
I'm trying to answer the following:
Show that $f(x,y)=x^y$ is primitive recursive.
Here's my try:
We can derive exponent thus:
$
f(x,0)=1, \ \ f(x,1)=f(x,0) \times x, \ \ f(x,2)=f(x,1) \times x, \ .....
- 197
0
votes
0
answers
29
views
Show multiply function is primitive recursive
I'm trying to answer the following question:
Show that $f(x,y)=xy$ is primitive recursive.
Basically, multiply function.
Here's my try:
To start with, we try to define it in terms of itself:
$$
f(x,...
- 197
0
votes
0
answers
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
0
votes
0
answers
13
views
A question involving generalized beta-conversion
Here's the question:
Show that if the only free variables in E are $x_1, .. , x_n$ and f, then if:
$$
\underline{f} = \underline{Y} (\lambda f(x_1, .., x_n). E)
$$
then
$$
\underline{f} (x_1, .., x_n) ...
- 197
0
votes
0
answers
21
views
Proving curried and uncurried functions
We are given
$$
\underline{add} \ \underline{m} \ \underline{n} = \underline{m+n}
$$
$$
\underline{mult} \ \underline{m} \ \underline{n} = \underline{m \times n}
$$
and
$$
\underline{sum} \ (\...
- 197
-1
votes
1
answer
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
0
votes
1
answer
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
0
answers
38
views
Solving Klop's fixed-point operator problem
The following problem is attributed to Klop mentioned in Barendregt's book (as per notes I'm going through).
Here's the problem:
Show that $\underline{Y_2}$ is a fixed-point operator, where
$$
LET \ @ ...
- 197
0
votes
0
answers
18
views
Show that a fixed point can be itself a fixed point operator
I want to show that a fixed-point $\underline{Y_1}$ defined as
$$
\underline{Y_1} = \underline{Y} \ (\lambda yf. f(yf))
$$
is a fixed-point operator.
ie. Show that
$$
\underline{Y_1} E = E (\underline{...
- 197
0
votes
0
answers
28
views
Deriving suc iszero pre functions from alternative definition of natural number
Here I am given an alternative definition for natural numbers.
Like this
$$
LET \ \widehat{\underline{0}} = \lambda x. x
$$
$$
LET \ \widehat{\underline{1}} = (\underline{false}, \ \widehat{\underline{...
- 197
1
vote
0
answers
19
views
Evaluating conditional expression
I want to show that
$$
(\lambda fgx. fx(gx)) (\lambda xy. x) (\lambda xy.x) = \lambda x. x
$$
Here's my try:
$$
(\lambda fgx. fx(gx)) (\lambda xy. x) (\lambda xy.x)
= (\lambda fgx. fx(gx)) \underline{...
- 197
2
votes
1
answer
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
0
votes
0
answers
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
0
answers
23
views
Evaluating iszero function
$\underline{iszero}$ function is defined as
$$
\underline{iszero} = \lambda n. n(\lambda x. \underline{false})\underline{true}
$$
I want to show that $\underline{iszero} \ \underline{5} = \underline{...
- 197
1
vote
0
answers
38
views
How can you construct lambda expression like λx. x+2 based on the definition given in Wikipedia.
From https://en.wikipedia.org/w/index.php?title=Lambda_calculus&oldid=1121552046#Definition :
How can I add operator like + or * ? Also based on the definition given, the Elements of $\Lambda$ ...
- 37
0
votes
0
answers
26
views
Evaluating expression for EXPONENTIATE
I want to show that
$$
EXP = \lambda mn. n (MUL \ m) \underline{1}
$$
by showing that $EXP \ \underline{m} \ \underline{n} = \underline{m^n}$.
EXP is for exponentiate and MUL is for multiply.
Here's ...
- 197
0
votes
0
answers
17
views
Proving lambda expression for multiplication
I want to show that
$$
MUL = \lambda mn. m(ADD \ n)\underline{0}
$$
by showing that $MUL \ \underline{m} \ \underline{n} = \underline{n \ * \ m}$.
Given that
$$
ADD = \lambda mn. (mS)n
$$
Here's my ...
- 197
0
votes
0
answers
22
views
Behaviour of successor function that is composition
I want to show that
$$
S^{m} \underline{n} = \underline{n+m}
$$
where $S$ is successor function and $\underline{m},\underline{n}$ are Church numerals. Note that $S^m (x) = \underbrace{S(S(..(S}_\text{...
- 197
0
votes
0
answers
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
0
answers
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
0
votes
0
answers
24
views
Generalizing lambda or expression
I want to generalize
$$
\underline{or} = \lambda xy. (x \to \underline{true} | y)
$$
to $\lambda AB. (A \to (\underline{true} \to ...) | B \to ...)$.
Here's my try:
Cases:
If A:
If B: $\underline{...
- 197
0
votes
0
answers
20
views
Good Way to Do Derivation for Lambda Calculus
I just found derive formula in lambda calculus is very difficult, at least on paper, because of the need to keep large quantity of symbols. Is there a better way to do the derivation? Maybe using ...
- 1,748
0
votes
0
answers
25
views
Algorithm for computing De Bruijn representation of substitution
I'm trying to answer the following question:
Describe an algorithm for computing the De Bruijn representation of the expression E[E'/V] from the representations of E and E'.
Here's my try:
Set $E=\...
- 197
0
votes
0
answers
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
0
votes
1
answer
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
0
votes
1
answer
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
0
votes
0
answers
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
-1
votes
1
answer
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
0
votes
0
answers
30
views
Valid substitution in lambda calculus
I'm trying to understand valid substitution in lambda calculus.
Is the following evaluation valid?
Let $V=V_1,V_2,V_3,V^*,V^{**}$ and $E=(\lambda V_1V_2V_3.V_1V_2V^*V^{**}V_3)$
Then I try to evaluate
$...
- 197
0
votes
3
answers
37
views
Lambda calculus Clarification about free and bound variables
In $(\lambda x.yx)$ y is free.
How about in $(\lambda x.xy)$ is y bound here? Some googling I've found that ...
- 197
0
votes
2
answers
59
views
Rules for beta conversion passing abstraction as parameter
Can you tell me why the following reduction is true?
$$
(\lambda x.yx)(\lambda y.xy)=yx
$$
I'm not quite sure about the rules to follow when abstraction $(\lambda y.xy)$ is applied to $(\lambda x.yx)$....
- 197
5
votes
1
answer
57
views
Need help understanding $\alpha$-equivalence.
I am currently reading through Type Theory and Formal Proof.
I see that there is some variation in the literature in the fine details on the discussion on how $\alpha$-equivalence is developed, such ...
- 1,041
1
vote
1
answer
31
views
Lambda calculus reductions
I encountered an example in lambda calculus:
$$(\lambda x.(\lambda y.(xy))x)(\lambda z.w)$$
Now, can I apply the second parenthesis to $\lambda x$? Then
$$(\lambda x.(\lambda y.(xy))x)(\lambda z.w) \...
- 299