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.

2
votes
0answers
12 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 ...
-3
votes
1answer
22 views

Arithmetic Operations - Lambda Calc [on hold]

Which arithmetic operation does the term $\texttt{$\lambda$n.$\lambda$m.m (MULT n) 1}$ compute?
-1
votes
1answer
21 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$ ...
0
votes
0answers
13 views

WHNF abstraction

I'm just posting this to verify my answer to the below question... If a closed term is a weak head normal form, it has to be an abstraction “\x.M”. Why? It has to be an abstraction because M ::= x |...
-1
votes
0answers
14 views

Reduction to Lambda Normal Form

How would I indicate whether the following lambda terms have a normal form: 1.) \x.(\y.yx)z)v 2.) (\x.xxy)(\x.xxy)
1
vote
1answer
16 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
27 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
44 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
32 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
29 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
82 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
33 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
42 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
46 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
35 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
33 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
25 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
21 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
64 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
46 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
56 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
61 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
23 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
37 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
35 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
36 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
29 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
64 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
56 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
41 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
16 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
92 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
79 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
49 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
39 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
95 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
82 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
42 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
93 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
274 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
407 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 ...
20
votes
0answers
457 views

Can a calculus have incremental copying and closed scopes?

A few days ago, I proposed the Abstract Calculus, a minimal untyped language that is very similar to the Lambda Calculus, except for the main difference that substitutions are ...
1
vote
1answer
82 views

How to transform lambda function to multi-argument lambda function and how to rewrite or approximate terms?

I am trying to do the formal semantics (Montague grammar, abstract categorial grammar) of natural language and encode the sentence John is boss. The type system has ...
1
vote
0answers
34 views

Call-by-push-value vs Fine-grain Call-by-value

It seems to me that Fine-grain call-by-value already subsumes CBV and CBN, using lambdas as thunks. What does CBPV improve upon FG-CBV or in what way is it "better"?
2
votes
1answer
82 views

Proving Progress for STLC with Linear and Unrestricted Types

In this paper Walker presents an extension of STLC with linear and unrestricted types. The proof of type soundness is left as an exercise to the reader. I encountered difficulty when attempting to ...