Questions tagged [lambda-calculus]
λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.
552
questions
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)
(...
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 ...
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:
...
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} ...
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 ...
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 ...
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 ...
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 ...
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 ...
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?
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))))))) (λ ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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'$ ...
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 ...
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 ...
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 ...
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:
...
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 ...
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:
...
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 ...
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 ...
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 ...
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 ...
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 ...
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:
$$ ...
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 := \...
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 ...
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$$
...
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 ...
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 ...
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.\...
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 ...
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 ...
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 ...
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"?
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 ...
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 ...
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)...
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 ...
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 ...
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 ...
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 ...
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?
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 (...
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:
...