Questions tagged [lambda-calculus]

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

Filter by
Sorted by
Tagged with
1 vote
1 answer
66 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) (...
Steven Noble's user avatar
5 votes
0 answers
134 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 ...
user56834's user avatar
  • 3,692
1 vote
1 answer
172 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: ...
zero_coding's user avatar
2 votes
1 answer
64 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} ...
Ben I.'s user avatar
  • 1,710
3 votes
2 answers
159 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 ...
Ben I.'s user avatar
  • 1,710
3 votes
1 answer
86 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 ...
MaiaVictor's user avatar
  • 4,127
1 vote
1 answer
486 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 ...
Ben I.'s user avatar
  • 1,710
1 vote
1 answer
48 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 ...
Maarten's user avatar
  • 13
1 vote
1 answer
54 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 ...
Marco's user avatar
  • 95
0 votes
2 answers
1k 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?
n0unc3's user avatar
  • 33
0 votes
1 answer
250 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))))))) (λ ...
Jay.F's user avatar
  • 55
6 votes
1 answer
365 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 provide logic ...
HappyFace's user avatar
  • 191
5 votes
1 answer
75 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 ...
Marco's user avatar
  • 95
5 votes
2 answers
266 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 ...
Christopher King's user avatar
4 votes
1 answer
272 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 ...
Christopher King's user avatar
1 vote
1 answer
174 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 ...
Sean's user avatar
  • 570
2 votes
1 answer
8k 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 ...
Dennis O's user avatar
4 votes
2 answers
387 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'$ ...
Christopher King's user avatar
3 votes
1 answer
58 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 ...
Sean's user avatar
  • 570
1 vote
1 answer
69 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 ...
warwcat's user avatar
  • 13
2 votes
1 answer
33 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 ...
Charlie Parker's user avatar
0 votes
1 answer
781 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: ...
Jan Parzydło's user avatar
0 votes
2 answers
417 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 ...
user avatar
0 votes
1 answer
327 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: ...
Jan Parzydło's user avatar
1 vote
0 answers
29 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 ...
Emanuele Giona's user avatar
10 votes
2 answers
345 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 ...
xavierm02's user avatar
  • 1,255
2 votes
2 answers
106 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 ...
Charlie Parker's user avatar
2 votes
1 answer
144 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 ...
Charlie Parker's user avatar
2 votes
0 answers
73 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 ...
Joey Eremondi's user avatar
2 votes
4 answers
605 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: $$ ...
Charlie Parker's user avatar
3 votes
2 answers
321 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 := \...
Delupara's user avatar
  • 143
13 votes
5 answers
3k 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 ...
MetaStack's user avatar
  • 327
0 votes
1 answer
43 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$$ ...
Alessandro Recchia's user avatar
3 votes
1 answer
52 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 ...
Sandro Lovnički's user avatar
5 votes
1 answer
859 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 ...
jack malkovick's user avatar
2 votes
1 answer
2k 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.\...
n0unc3's user avatar
  • 33
3 votes
2 answers
3k 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 ...
jack malkovick's user avatar
23 votes
0 answers
1k 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 ...
MaiaVictor's user avatar
  • 4,127
1 vote
1 answer
164 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 ...
TomR's user avatar
  • 1,381
2 votes
1 answer
287 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"?
Labbekak's user avatar
  • 565
2 votes
1 answer
139 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 ...
emi's user avatar
  • 123
4 votes
0 answers
454 views

CFG for $\lambda$-calculus with minimal parentheses

The typical presentation of the syntax of the $\lambda$-calculus is as an ambiguous CFG (or BNF) like the following: $$T \rightarrow \lambda X . T \mid T ~ T \mid X \mid (T)$$ Where we permit $X$ to ...
Cameron Moy's user avatar
4 votes
1 answer
96 views

if an argument of a lambda only passes itself if it is further evaluated, is runtime always finite?

In order for a lambda expression to run forever, there must be at least one lambda in the expression in which an argument is passed to itself. For example the following runs forever. $$ (\lambda x.xx)...
rtpax's user avatar
  • 141
2 votes
2 answers
301 views

Confusion about the definition of de Bruijn terms in the TAPL book

I'm working through Types and Programming Languages right now, and I'm a little confused about the recursive definition given for nameless/de Bruijn terms (chapter 6, definition 6.1.2). Below is the ...
MattDs17's user avatar
  • 123
5 votes
2 answers
1k views

Why is abstraction in lambda calculus called abstraction?

The term abstraction as I understand it, is used in many different contexts, but has one essential meaning, namely that it refers to the “general properties of some class of objects that doesn’t rely ...
user56834's user avatar
  • 3,692
4 votes
2 answers
450 views

In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?

I am trying to infer the type and prove that this is well-typed: let $f =\lambda x.x$ in $f f$ Obviously the $f$ is the identity function, so it's the same as let $id =\lambda x.x$ in $id$ $id$ I ...
MiragePV's user avatar
2 votes
0 answers
42 views

Understanding First conversion rules from church's lambda bible

While going through Church's text on Lambda calculus , I cam across the first set of conversion rules . Before writing out my query I would like to put the notation that church has used for ...
Agnivesh Singh's user avatar
0 votes
0 answers
68 views

how to build logical representation from dependency tree

I'm trying to build logical representation from dependency tree with python. i created the tree with stanford parser. How can I derive logical presentation from it using Lambda-calculus?
LY-'s user avatar
  • 1
2 votes
0 answers
355 views

Term for weak head normal forms that cannot be reduced in any environment

In my understanding, a lambda expression is a normal form (NF) when it has no redexes. For instance, $\lambda x.x$ is a NF, but $(\lambda x.x)y$ is not. A lambda expression is a weak head normal form (...
user avatar
1 vote
2 answers
307 views

Application of lambda function in Simply Typed Lambda Calculus

I'm just getting started with STLC (Simply Typed Lambda Calculus) and I'm trying to understand an evaluation rule I've been given in some lecture notes by my professor. What it says is the following: ...
Nyfiken Gul 's user avatar

1
3 4
5
6 7
12