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.

1
vote
1answer
40 views

Relation of self-application to non termination in the untyped lambda calculus.

I was reading the following question: Self-application in Church's untyped lambda calculus First, we can have terms which, if applied to themselves, still have normal form. For example, $(\lambda ...
-2
votes
0answers
10 views

Can someone give me a hint on how to solve this lambda calculus related question?

et TRUE = \x y -> x let FALSE = \x y -> y let ITE = \b x y -> b x y let NOT = \b x y -> b y x let AND = \b1 b2 -> ITE b1 b2 FALSE let OR = \b1 b2 -> ITE b1 TRUE b2 -- YOU SHOULD ONLY ...
1
vote
0answers
24 views

Can induction be proven in $\lambda C$?

Is it possible to prove induction in $\lambda C$? In other words, is the following type inhabited? $$\Pi P:\mathbf{nat} \to \ast. (P0 \land \Pi n : \mathbf{nat}. Pn \to P(\mathbf{succ}\ n)) \to \Pi n ...
1
vote
1answer
22 views

Are these 2 lambda calculus terms equivalent?

I have 2 lambda terms and I am not sure whether the rules of bounded variables in the lambda calculus imply that these 2 terms are equivalent or not. They are: $λc.λc.bc$ $λc.λa.ba$ I know that ...
0
votes
1answer
39 views

Is expression evaluated before assigning type?

I am assigning type to an $\lambda$-expression: if false then M else N where if A then B else C and ...
0
votes
0answers
35 views

Is there an ordering of logical systems defined by reductions?

I am aware of the lambda cube which gives an ordering to several variants of the lambda calculus. My intuition says that this ordering should have the following property: For logics $A,B\in\lambda\...
2
votes
2answers
74 views

Syntactic proof that Peirce's law doesn't hold in simply-typed lambda calculus

This might have been asked before, but certainly I don't find any source. Even in the literature I've consulted, there is no such proof so far. Context In the context of the simply typed lambda ...
-1
votes
1answer
19 views

Brackets in Lambda Calculus with multiple lambdas

How would you evaluate $\lambda x.\lambda x.\lambda x.x 1 2 3$? I cant figure out if the first lambda takes the 1 beta reduces, then the second lambda takes the 2 then beta reduces and finally the ...
1
vote
1answer
39 views

Recursive Definition of Normal Form with explicit substitution

Context I assume a simply typed lambda calculus, probably written with de-bruijn indexes. With $\to_\beta$ I denote the $\beta$-reduction as a relation. Also, my question eventually will use this $\...
1
vote
1answer
30 views

Scope of the first x in $(\lambda x. (\lambda x. x x) \ (\lambda x. x x))$

I want to reduce this to normal form. I think it's already in normal form, but that one can get the same expression infinitely. But that necessarily means the first $x$ does not bind any of the inner ...
3
votes
2answers
47 views

Lambda Calculus: Reduce $(\lambda x. (\lambda y. x \ y) \ x) \ (\lambda z.p)$

According to the answer sheet it is supposed to reduce to $p$, but I dont know how. This is what I do $$(\lambda x. (\lambda y. x \ y) \ x) \ (\lambda z.p)$$ I replace $x$ with $(\lambda z.p)$ $$\...
0
votes
0answers
12 views

Partial derivative of a function within a function, lambda calculus

$$ L = u_1 (x_1,y_1) + \lambda \left[ u_2(x_2, y_2) - u_0^2 \right] + \mu \left[0 - T(x_1,x_2,y_1,y_2) \right] $$ $\lambda$ and $\mu$ are the multipliers. There's a number of variables to partially ...
0
votes
0answers
159 views

Theorem on alpha conversion in type free lambda calculus

I am going through Lemma 1.2.11 of "Lectures on the Curry-Howard Isomorphism" by Morten Heine Sørensen and Pawel Urzyczyn. There is a free sample that includes this lemma here: https://play.google.com/...
1
vote
1answer
53 views

Formal definition of substitution being defined in type free lambda calculus

In "Lectures on the Curry-Howard Isomorphism" by Morten Heine Sørensen and Pawel Urzyczyn, it is stated that: The substitution of $N$ for $x$ in $M$, written $M [ x := N ]$, is defined iff no free ...
0
votes
1answer
23 views

Use of parenthesis in the body of abstraction in lambda expression

In the lambda expression $(λx. (λy. (x y)) y) z$, the body of the abstraction is taken as $(λy. (x y))y$ and not just $(λy. (x y))$. Why isn't $(λy. (x y))$ considered as the body and the following $...
0
votes
0answers
42 views

What does the first “non-free” variable mean here when substituting in simple type theory?

See this screenshot of the book "Basic Simple Type Theory". The infinite sequence they refer to is just a way to formalize the concept of having enough variables to work with no matter what. In my ...
2
votes
1answer
65 views

Can we see categories as programming languages?

In this video, category theory is explained to an audience of programmers. The speaker says that we can think of a category as a programming language, and of objects as types in that language, and ...
1
vote
1answer
61 views

predecessor and multiplication prove

I have trouble, when attempting to : 1- prove mult defines the multiplication function. 2- Prove pred defines the predecessor function. 1- for mult: Base Case: mult 0x= 0 Inductive case: := $(\...
0
votes
1answer
23 views

Thinning lemma in simply typed lambda calculus

From "Type Theory and Formal Proof" by Rob Nederpelt and Herman Geuvers: Definition 2.4.2 (1) A statement is of the form $M : \alpha$, where $M \in \Lambda_{\mathbb{T}}$ and $\sigma \in \...
1
vote
1answer
52 views

lambda calculus evaluation

I have a question about lambda calculus. I just read that it doesn't matter in which way expressions get evaluated. So my question is: $(\lambda f.\lambda x.f(fx)) (\lambda y.y+1) 2$ so we can ...
1
vote
0answers
25 views

exhibiting a turing machine and a λ-term of a boolean function

I have a funtion f: BOOL ⇒ Bool, sich that f(x,y) is true when x=y and false otherwise. Im trying to exhibit a touring machine and a lambda term. for the second part I know that in boolean logic, x ⇒ ...
3
votes
0answers
37 views

Type equivalence in $\lambda\underline\omega$ under lambda abstraction

I'm going through "Type Theory and Formal Proof" by Nederpelt and Geuvers and just trying to play around with $\lambda\underline\omega$ after reading the chapter on it to better grasp the material. ...
0
votes
0answers
14 views

Lemma relating to alpha equivalence of lambda terms

From Type Theory and Formal Proof, An Introduction by Rob Nederpelt and Herman Geuvers: Lemma 1.7.1 Let $M_{1} =_{\alpha} N_{1}$ and $M_{2} =_{\alpha} N_{2}$. Then also: (1) $M_{1}N_{1} =_{\alpha} ...
1
vote
1answer
68 views

Ambiguity of definition of substitution in lambda calculus

From Type Theory and Formal Proof, An Introduction by Rob Nederpelt and Herman Geuvers: Definition 1.6.1 (Substitution) (1a) $x[x := N] \equiv N$, (1b) $y[x := N] \equiv y$ if $x \not \equiv y$, (...
0
votes
0answers
45 views

Definition of renaming in lambda calculus

From "Type Theory and Formal Proof, An Introduction" by Rob Nederpelt and Herman Geuvers: Definition 1.5.1 (Renaming; $M^{x \to y}$; $=_{\alpha}$) Let $M^{x \to y}$ denote the result of replacing ...
0
votes
1answer
32 views

Is there a right identity for Application in Lambda calculus?

Such a function E that: ∀F (F E = F) It's obviously, that the left identity E' (E' F = F) ...
4
votes
2answers
47 views

Help understand beta reduction example

I am currently reading a text book on distributed computing systems that includes a short introduction to $\lambda$-calculus. There is an example of evaluating the sequence $(((if \space \space true) ...
1
vote
0answers
36 views

beta reduction: order of substitution

Do we always apply our input to the left most term in a lamda expression? For instance, take the expressions: $λP λQ. ∀x P(x)→Q(x)$ which we can rewrite as $[λP λQ[ ∀x P(x)→Q(x)]]$ $λP. λQ. ∀x P(x)→...
2
votes
2answers
86 views

Evaluate this alpha substitution $[(zx)/x] \, \lambda z.xyz$

I am having difficulty with the following problem: Calculate the result of this substitution, renaming the bound variables as needed, so that substitution is defined $[(zx)/x] \, \lambda z.xyz$ ...
2
votes
1answer
66 views

How many possible Beta-reductions considering order of the expression $(\lambda x.\lambda y.y)(\lambda x.x) ((\lambda x.x) (\lambda y.y))$

Here is a lamba calculus expression: $(\lambda x.\lambda y.y)(\lambda x.x)((\lambda x.x) (\lambda y.y))$ For simplicity let $a:=(\lambda x.\lambda y.y)$ $b:=(\lambda x.x)$ $c:=(\lambda x.x)$ $d:...
5
votes
1answer
39 views

Beta reduction for expression

I'm given the following where: TRUE = λxy.x FALSE = λxy.y IF = λbtf. b t f OR = λxy. IF x TRUE y and I'm trying to evaluate: ...
1
vote
0answers
70 views

The continuation passing style transformation in the lambda calculus

I have an issue understanding the following definition (from https://tel.archives-ouvertes.fr/tel-00783245/document , p.82) of the continuation-passing style (CPS) transformation in the lambda ...
0
votes
0answers
53 views

Determining type of composed function

We would like to know the type of the function composition $f \circ f$. The function in question is typed as follows: $f :: (\alpha \rightarrow \beta \rightarrow \gamma) \rightarrow (\alpha \times \...
3
votes
1answer
47 views

(𝜆x. (𝜆y. y)) (𝜆a. (𝜆b.a)) beta reduction

I've came across an example and I'm not quite sure on how the solution was met after performing beta-reduction on the following expression. It doesn't show any of the steps. Any help is appreciated! (...
1
vote
1answer
95 views

Reducing Lambda to Normal Form

I'm having issues trying to reduce (λx. (λy. y x) (λz. x z)) (λy. y y) to its normal form. I get to ...
0
votes
0answers
35 views

Function in Lambda Calculus

Yesterday I have been trying to complete this exercise. I have to find: $$ ((map)l)t \simeq \lambda k \lambda x ((k)(t)t_1)....((k)(t)t_n)x $$ where $$l=\lambda k \lambda x ((k)t_1)....((k)t_n)x$$ ...
2
votes
1answer
68 views

How to find a simple function in Lambda Calculus?

I was doing this exercise : Find the function $$exchange$$ such that: $$(exchange)t \simeq \lambda p(p)t_2 t_1$$ where $$t= \lambda p(p)t_1 t_2.$$ I found $$ exchange= \lambda p(p) (\lambda c (S \ \...
2
votes
1answer
41 views

$(M B) (M B)$ canonical form

Are there lambda terms $M$ and $B$ with $M \neq B$, so that $M B$ and $(M B) (M B)$ have the same canonical form? Is a problem I encountered while I am still new with lambda calculus I approached ...
2
votes
1answer
113 views

what are the 5 simplest lambda calculus expresions

I'm struggling to learn lambda Calculus. I think what might really help is to see the simplest functions that you can create in lambda calculus and how they might be combined to make more complex ...
6
votes
2answers
75 views

In rewiring systems do definitions creates new rewrite laws or an alias? And is this a meaningful question?

Lambda calculus is often introduced as a rewriting or substitution system. Where $\beta$ reduction is described as replacing bound variables with the value that variable is bound to. For example $(\...
-1
votes
1answer
91 views

Why does Turing-computing (being an inconsistent formalism) has undecidable problems? [closed]

I'd like to apply Church-Turing thesis to Kleene-Rosser paradox: Since untyped lambda-calculus is an inconsistent formalism AND Turing machines are equal in decisive power to lambda-calculus SO We ...
3
votes
1answer
84 views

In Homotopy Type Theory, where does the lambda expression reside?

Background I am trying to develop a visual language for doing higher level mathematics. The language is essentially the language of categories with some allowances since this thing runs on a ...
0
votes
1answer
124 views

What is the meaning of this Church numeral example?

There is an example of Church numeral, on the secion Encoding Datatypes of lambda calculus's wikipedia page. One way of ...
1
vote
1answer
74 views

Confused by the explanation of beta reduction of lambda calculus on wikipedia.

On this wikipedia article, there is an explanation of lambda calculus. In the section of Beta reduction, there is an Omega ...
2
votes
0answers
46 views

Transformations similar to Curry/Uncurry

The currying operator transforms a function of the form $(A\times B)\rightarrow C$ into an equivalent one of the form $A\rightarrow(B\rightarrow C)$. The uncurrying operator goes the other way round. ...
2
votes
1answer
93 views

Is it possible to express syntactic equality function in lambda calculus?

Let's denote truth and false by two suitable constants $T, F$ where $T \not=_\beta F$ where $\equiv$ is syntactic identity. Could I define a $\lambda$-term $E$ such that for $\lambda$-terms $X$ and ...
5
votes
1answer
97 views

Is there a standard notation for the pre-composition operator?

Let $X_1$, $X_2$, and $V$ be sets. Is there a standard name and a standard notation for the pre-composition operator $F$ that takes as input a function $\varphi:X_2^{X_1}$ and returns the operator $F_{...
2
votes
1answer
201 views

Y combinator as an application of Lawvere's fixed point theorem

Lawvere's fixed point theorem states that that in a cartesian closed category, if there is a morphism $ϕ: A \to B^A$ which is point-surjective (i.e., for every point $q : 1 \to B^A$ there exists a ...
1
vote
0answers
35 views

Help express this λ-calculus function in a non-recursive form?

The function is fib = λn(IF (n<2) 1 (fib(n-1)+fib(n-2)) (if n<2 then 1, else the sum of the previous two). How do I make it non-recursive? I know it's about ...
6
votes
1answer
76 views

What categories are described by relational programming languages?

I know that lambda calculus is the language of cartesian closed categories. As I understand it, relational programming systems (that, as the name implies describe a computation in terms of relations) ...