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]

λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.

4
votes
1answer
40 views

Why 'let' can not be reduce to a lambda application in (extended) Calculus of Constructions

I do not understand the difference highlighted in the chapter 2.5 of the book Theorem Proving in Lean: Notice that the meaning of the expression let a := t1 in t2 is very similar to the meaning of (...
1
vote
2answers
73 views

What are the other language models of computation similar to lambda calculus?

I hope this question makes sense, but I was wondering if there are other models of computation similar to lambda calculus that you can use to build up axiomatic mathematical and logical fundamentals ...
3
votes
2answers
91 views

Check if a lambda constructor is well-typed

In basic type inference for 𝜆-calculus with parametric polymorphism à la Hindley–Milner, when can we say that we cannot give a type to a lambda constructor? For example $$(λx.λy.y(x\ ...
2
votes
1answer
45 views

Variable Capturing With Repetition of Variable Name

I am very confused as to which variables are captured by which λ in the example below: (λa.λb.(λa.a)aba)(ab) I am new to lambda calculus and the repetition of ...
5
votes
2answers
92 views

Are there lambda-calculus functions which always output booleans, but are not constant functions?

In labmda calculus, true = $\lambda x,y.x$ and false = $\lambda x,y.y$. Is there a term $f$ such that for any other term $x$, $f x$ normalizes to true or false BUT $f$ does not have the same output ...
2
votes
1answer
37 views

Must a function in lambda-calculus which inputs a boolean function be defined in a certian way?

This question is my best attempt to get at a more general question about what one can get from terms in the lambda calculus. Using the church encoding, we define booleans by $\texttt{true} = \lambda ...
5
votes
0answers
26 views

Unbounded-time programs in lambda calculus?

The Turing machine model has been extended to “infinitary turing machines”, which are Turing machines that can perform a countably and uncountably infinite amount of computations in finite time. Is ...
2
votes
0answers
20 views

Construct a lambda term from a Böhm tree

Given an acyclic graph, how can I build a lambda calculus term such that this graph is the term's Böhm tree? If the Böhm tree is a finite tree (so the result is a strongly normalizing term). If the ...
-1
votes
1answer
24 views

Reduce to Beta Form Verification

What is the normal form of the following lambda term? I'm stuck between two answers and I just wanted to know which one is correct. $$\lambda y. (\lambda x.x)\ y$$ Possible Answer 1: $\lambda x.x$ ...
1
vote
1answer
29 views

What do the symbols M and N mean in this definition of lambda terms?

I am learning lambda calculus from the book https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-Lambda-Calculus-Notes.pdf and do not understand the meaning of the following symbols. The ...
0
votes
2answers
37 views

No Lambda Normal Form

How can we show that the term $\Omega = (\lambda x.x\ x)\ (\lambda x.x\ x)$ does not have a normal form? Building on this, what is an example term different than Omega that is not normalizing (meaning ...
5
votes
0answers
53 views

Difference between “functional programming languages” and “lambda calculus based languages”?

In "Can programming be liberated from the Von Neumann Style?", John Backus states: The main reason FP systems are considerably simpler than either conventional languages or lambda-calculus-based ...
0
votes
1answer
41 views

What's a general rule for this little lambda calculus identity?

I've been fiddling around with a project that does some normalization of lambda calculus(-like) expressions and I stumbled upon that (λ λ ... λ n (n-1) ... 2 1) (...
4
votes
0answers
41 views

What is a “model” of lambda calculus?

I know about the concept of the "model" of a logical proposition in the context of mathematical logic: It is a mathematical structure in which that proposition is true. However, it's not clear to me ...
1
vote
1answer
93 views

What does all uppercase letters mean?

I am reading https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-Lambda-Calculus-Notes.pdf and would like to know, what the following statement means: ...
2
votes
1answer
34 views

Church numerals without functions

This is really a second part to my first question, but I felt that this was different enough from the first part that it merited its own question. So, using Church numerals, we define $3 = {\lambda} ...
3
votes
2answers
44 views

Is there a systematic way to know when to alpha-transform free variables?

So, using Church numerals, we define $3 = {\lambda} f. {\lambda}x.f(f(f(x)))$, and $4 = {\lambda} f. {\lambda}x.f(f(f(f(x))))$. We can then add with an expression like $3\ g\ (4\ g\ z)$ And ...
3
votes
1answer
47 views

What are different ways to provide a semantics to a language?

Suppose you have 1. a grammar for terms of a language; 2. type-assignment rules, 3. a set of reduction rules. You want to prove that your language is adequate for mathematical reasoning. If I ...
1
vote
1answer
45 views

lambda expressions, parenthesis, and order of application

I am building a lambda applicator in Java, and I have uncovered a bit of misunderstanding. Either my question at the bottom is what I am asking, or something in the build-up below is wrong. Either ...
1
vote
1answer
34 views

Tailrecursive definition for a function

In an exam I took we were asked to provide a tailrecursive definition of a recursive function. I failed miserably and the provided solution makes absolutely no sense to me. If anyone could explain ...
0
votes
0answers
25 views

Computational type theorists: how do you compare terms for equality here?

I am attempting to implement Simple Type Theory in the language D. How do you compare subterms to a term $R$ for the sake of computing the covering abstractors of $R$ in $M$? By reference (class ...
1
vote
1answer
24 views

Lambda term satisfying two equations using Bohm Trees

Hi I'm trying to solve this exercise but I can't find any material online, it's not an homework I actually have sort of a solution (it looks incomplete though), but from that I can't really understand ...
0
votes
2answers
47 views

Beta reduction order in Lambda calulus

Will it be wrong to use g for reducing (λx.λy.x) first in step (2) instead of using to reduce λg? Is there a rule against it?
0
votes
1answer
37 views

is reducing to normal form simply applying beta-reduction?

See example below: reduce to normal form: (λ c . (λ a . (λ d . (λ h . (h (d (a (a (λ z y . y))) (d (a (a (λ f x . x))) (a (a (a (λ z x . x)))))) (h (a (a (λ z y . y))) (a (a (a (λ z x . x))))))) (λ ...
4
votes
1answer
69 views

Why are there two not operators in lambda calculus?

From Wikipedia: $\mathrm{true} = \lambda a. \lambda b. a$ $\mathrm{false} = \lambda a. \lambda b. b$ Because true and false choose the first or second parameter they may be combined to ...
5
votes
1answer
47 views

Find a lambda term satisfying two equations

I'm just looking for the general idea on how to approach the following problem: Find a term $\Delta=\lambda x.xUV$ such that: $\Delta\Delta=K$ $\Delta K=S$ (it's a system of 2 equations, I didn't ...
1
vote
2answers
62 views

Elegant algorithm to semi-decide if two lambda calculus terms are equivalent

Given two lambda terms $t_1$ and $t_2$, it is semi-decidable if they are equivalent (i.e. can be rewritten as each other using alpha, beta, and eta conversions). An algorithm to do this is to try ...
3
votes
1answer
67 views

Efficient algorithm to determine if a lambda calculus term is equivalent to one without a given free variable

Consider the following problem: given a lambda calculus term $t$ and free variable $v$ determine whether $\phi(t,v)$, where $\phi(t,v) := \exists t'. t' \equiv t \land v \notin FV(t')$. This problem ...
1
vote
1answer
37 views

Evaluation of $\beta$-Reduction with Parentheses in $\lambda$-Calculus

I'm studying $\lambda$-calculus, and had a question regarding an exercise I came across. I understand that $\lambda$-calculus uses three main strategies of evaluation, but I'm having trouble applying ...
0
votes
1answer
104 views

Lambda Calculus - Call-by-name AND call-by-value reduction

I have been tasked with reducing the following lambda expression: (λpq.pqp)(λab.a)(λab.b) using call-by-name and call-by-value reduction strategies. Call-by-name strategy: Left-most, outermost ...
2
votes
2answers
38 views

When are you supposed to eta-reduce?

Wikipedia lists the following algorithm for normalizing a lambda calculus term $t$: If $t$ is not in head normal form, beta reduce the beta redex in the head position to get $t'$. Then normalize $t'$ ...
2
votes
1answer
29 views

Why do we have to make variables unique when evaluating $\lambda$-calculus?

I'm studying $\lambda$-calculus and came across a problem that I'm not sure how to understand. More specifically, it's about evaluating $\lambda$-calculus expressions using $\beta$-reduction. I was ...
1
vote
1answer
37 views

Can two free variables in lambda calculus have different values?

I am studying lambda calculus for the first time and I was trying to do the reduction beta of the lambda term $(\lambda x.xy)y$. Can I assume that these two free variables $y$ are the same? Or do I ...
2
votes
1answer
30 views

What are some concrete examples of what typed lambda constants are?

I was reading the following and found the following paragraph that I didn't understand: Let us also consider a set Σ of typed λ -constants, that is, pairs σ : t, where t is some type. Like for ...
0
votes
1answer
101 views

Handling epsilon productions in recursive descent parsing

I am working on a recursive descent parser for lambda calculus. In my grammar, after removing left-recursion, I am left with the following two productions: ...
0
votes
2answers
71 views

Multiple inputs in lambda calculus (Confusing example)

In a programming class I take, we briefly (very briefly) touched lambda calculus. I think I have a pretty good grasp of the basics now, but one example given I just don't understand. Am I missing ...
0
votes
1answer
52 views

Is this a correct grammar for untyped lambda calculus?

I am trying to write a recursive-descent parser for untyped lambda calculus. While researching the way of formulating the grammar, I managed to put together something like this: ...
1
vote
0answers
18 views

Combinatory Logic formula obtained from lambda term, proof?

I translated the following $\lambda$-term: $z(\lambda b.ba)(tt)(\lambda y.y)$ in the following CL formula: $z(CIa)(tt)I$ through the Markov algorithm. Now I'd like to prove the translation was ...
10
votes
2answers
97 views

Confluence of beta expansion

Let $\to_\beta$ be $\beta$-reduction in the $\lambda$-calculus. Define $\beta$-expansion $\leftarrow_\beta$ by $t'\leftarrow_\beta t \iff t\to_\beta t'$. Is $\leftarrow_\beta$ confluent? In other ...
2
votes
2answers
83 views

How does one show $(\lambda x . (\lambda y.x))yx \equiv_{\beta} y$ in lambda calculus?

I wanted to show: $$ (\lambda x . (\lambda y.x))yx \equiv_{\beta} y $$ the definition of beta equivalence is on page 17 of these notes. I did a few attempts but got different things like $x$. I ...
2
votes
1answer
52 views

How do we show $\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x . x)$ in lambda calculus?

How do we show $$\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x . x)$$? I was going through the slides here and it asked to do the above but by page 16 of the slides we have not ...
2
votes
0answers
42 views

Are there any interesting terms in pure LF or $\lambda\Pi$?

In my searching, I've seen that if Church numerals are encoded in a dependently typed Lambda calculus, that we can't derive induction or that $0 \neq 1$. I know that LF and the dependently typed ...
2
votes
4answers
103 views

How does one formally show that two lambda functions are $\alpha$ equivalent?

I was going through the following slides and I wanted to show the following: $$ \lambda x. x \equiv_{\alpha} \lambda y . y$$ formally. They define a an $\alpha$-conversion on page 15 as follows: $$ ...
2
votes
2answers
88 views

Why is it that a lambda function requiring multiple input also requires multiple functions?

So I recently discovered lambda calculus and for the most part I understand it. However, one specific part of it that I cannot understand is this: Let's say we define a very simple function $$ I := \...
10
votes
5answers
2k views

Lambda Calculus Generator

I don't know where else to ask this question, I hope this is a good place. I'm just curious to know if its possible to make a lambda calculus generator; essentially, a loop that will, given infinite ...
0
votes
1answer
31 views

How to find a 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$$ ...
3
votes
1answer
43 views

Why does existence of predecessor imply adequacy of a numeral system?

I encountered this result when working with $\lambda$-calculus (so every element I mention here was a $\lambda$-expression there [1]), but I will express everything with, more understandable to ...
2
votes
1answer
120 views

Differences between Church and Scott encoding

I'm kind of new to lambda calculus and I found this Wikipedia article https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding The section Comparison to the Church encoding presents a short ...
2
votes
1answer
419 views

Reducing lambda expression to normal form

Can someone explain the steps to reduce $$ (\lambda n. \lambda m. \lambda f. \lambda x.\ n\ (m\ f)\ x)\ (\lambda f. \lambda x.\ f\ (f\ x))\ (\lambda f. \lambda x.\ f\ x) $$ to $\lambda y. \lambda z.\...
2
votes
2answers
467 views

Encoding (binary) trees using lambda calculus

I'm new to lambda calculus, and I read all kinds of interesting stuff about encoding data types as functions. Church booleans, numbers and lists. https://en.wikipedia.org/wiki/Church_encoding Is ...