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.

2
votes
2answers
31 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
15 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
32 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
27 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 ...
2
votes
2answers
32 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
11 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
155 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
52 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
0answers
18 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
41 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
62 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
54 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
20 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
50 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
64 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
39 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
31 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
44 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
29 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
60 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
36 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
63 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
52 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
46 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
83 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
67 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
38 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
105 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
74 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
79 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
81 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
103 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
67 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
87 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
94 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
189 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
34 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) ...
5
votes
2answers
73 views

Can all mathematical operations be encoded with a Turing Complete language?

In High School Computing I was taught the Structured Program Theorem - that you could implement any mathematical operation using: Sequence Selection Iteration After completing a Computer Science ...
1
vote
0answers
50 views

Confused about applicative order

Applicative order is said to be leftmost, innermost. But I often here, it means "first evaluate the arguments". Sometimes I'm confused to what actually applies in what case. Here's an example: $$(...
3
votes
0answers
61 views

Head position in lambda calculus

I'm confused about what actually constitutes the head position in a lambda term. Wikipedia defines it as the $(\lambda x. A) M_1$ in: $\lambda x_1 . \ldots \lambda x_n . (\lambda x . A) M_1 M_2 \...
1
vote
2answers
98 views

Lambda Calculus Syntax - Brackets between $\lambda$ and dot

I just realised that I have a very trivial/basic question concerning the syntax of Lambda Calculus. Question 1: Is possible to have brackets between a lambda symbol, i.e., "$\lambda$" and a dot "$....
0
votes
1answer
95 views

How far does $\eta$-reduction go?

A term is is normal form, if there are no more redexes. But I'm confused as to what that means. E.g. $\lambda x. f x$ isn't in normal form, obviously, because it contains an $\eta$-redex. But is $\...
0
votes
1answer
40 views

Flipping to terms in lamda calculus

I am very new to the concept of lambda calculus. My question is mainly about the first bracketed term in the below expression. The first term is supposed to flip the next two terms but I feel uneasy ...