Stack Exchange Network

Stack Exchange network consists of 174 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.

0
votes
1answer
13 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
25 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
21 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
23 views

$\lambda$ term to return true if x = y otherwise return false

can someone please tell me how can i write $\lambda$ term that return true if x = y, and return false otherwise addition help for turing machine would be highly appreciated. Bests
3
votes
0answers
33 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
13 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
58 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
35 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
27 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
43 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
20 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
83 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
51 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
55 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
51 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
44 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
44 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
64 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
36 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
95 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
71 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
76 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
78 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
78 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
57 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
77 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
90 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
161 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
65 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
40 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
50 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
77 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
76 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
35 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 ...
0
votes
0answers
63 views

Hindley and Seldin “Introduction to Combinators and Lambda calculus”: Question about the solution to exercise 3.5.

The question is concerning the solution to exercise 3.5. In the exercise, they ask us to prove that any finite set of simultaneous equations $x_iy_1...y_n=Z_i$, where $1\leq i\leq k$, can be solved ...
1
vote
1answer
67 views

Why is $\lambda x.\lambda y. x y$ $\alpha$-equivalent to $\lambda x. \lambda y. yx$?

Why is $\lambda x.\lambda y. x y$ $\alpha$-equivalent to $\lambda x. \lambda y. yx$? Can we prove it by strict steps based on the definition of $\alpha$-equivalence in the $\lambda$-calculus?
2
votes
1answer
62 views

Variable Condition in Typed Lambda Calculus

tl;wr In which way does the variable condition for the typing of $\forall_x$, carried over by the $\forall_x$-introduction rule, limit the type setting? Is there more to it then keeping it in line ...
3
votes
1answer
94 views

Lambda Calculus – Defining lambda term to represent function $f(n) = true$ if $n$ even and $false$ otherwise

I have a problem with Exercise 7 from Selinger's notes on Lambda Calculus. Here there is the exercise: Find a lambda term that represent the function: $$f (n) := \begin{cases} \mathbf{T}, \text{ ...
1
vote
1answer
159 views

Lambda Calculus – Defining (and checking) Predecessor combinator for Church numerals

Studying Lambda Calculus I stumbled upon the problem of defining the predecessor combinator for Church numerals, i.e., the operation that produces as output the Church numeral that immediately ...
2
votes
0answers
68 views

Lambda Calculus - Exercise with fixed point combinator

This is exercise 2.10(iii) from "Introduction to Lambda Calculus". We need to find an $F$ such that $F \mathbf{I} \mathbf{K} \mathbf{K} = F \mathbf{K}$ Here there is my solution: Let $\mathbf{K}_3 ...
1
vote
1answer
48 views

Lambda-Calculus - Alternative proof without fixed point combinator

New chapter in my struggle with Lambda Calculus (previous chapters here and here, with my great thanks to those users who wrote enlightening answers). My problem is now to establish the following ...
1
vote
1answer
55 views

Lambda-calculus - Basic Problem with application of Fixedpoint theorem

This question is a sort of follow-up of a previous one. Again, I just do not really see how the $\lambda$-calculus actually works. Now, the problem is with Example 2.13 at page 12 of Introduction to ...
2
votes
1answer
77 views

Lambda calculus, $M$ doesn't have a normal form, $N$ has normal form. Find $M N$ that has a normal form?

I'm trying to understand more about $\lambda$-calculus through exercises so I'm stuck with this one: Being: $M$ a $\lambda$-term without normal form (we can't find a normal form, such as the term $(...
2
votes
0answers
49 views

Lambda Calculus and naming

I see that $\lambda$-calculus let's you work with anonymous functions and names are purely local. As an example $$\lambda x.x$$ contains $x$ only as a local name. This will be replaced during ...
1
vote
1answer
107 views

Devising Multiplication in Untyped Lambda Calculus

I am trying to learn basics of lambda calculus by following the tutorial by Raul Rojas, called A Tutorial Introduction to Lambda Calculus. In it, I have reached the Arithmetic section. We defined ...