λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.
5
votes
2answers
173 views
What is, exactly, $\lambda$-calculus?
I'm starting an undergraduate computer science course next fall, but I can't really understand λ-calculus in the context of functional programming. I may be misinterpreting this completely, but based ...
3
votes
1answer
35 views
Are there a lambda-mu expression equivalent to the yin yang puzzle?
The yin yang puzzle was written in Scheme. Since it uses call/cc, it is not possible to express it in a pure lambda expression, unless we do a CPS transform.
However, given the fact that λμ-calculus ...
0
votes
1answer
51 views
Free and bound variables in a lambda-calculus term
For this term:
$\lambda x.(f (g x))$, what are the free and bound variables?
I'm confused as to how to expand this so it will be easier to see.
If I expand this will it be $\lambda x. \lambda ...
1
vote
1answer
52 views
A program that cannot be written in (simply-)typed lambda calculus but only in lambda calculus or Turing-complete language
Programmers do sometimes write a program that creates infinite loop if some particular input is passed into the program.
But Simply-typed lambda calculus has to stop - so the question is, can anyone ...
2
votes
1answer
34 views
Free and Bound in Lambda Calculus
Here's something from Slonneger's "Syntax and Semantics of Programming Languages":
A variable may occur both bound and free in the same lambda
expression: for example, in λx.yλy.yx the first ...
3
votes
1answer
60 views
Substitution by structural recursion
Following the article's notation, I write $\mathcal{F}$ for the
category of presheaves on a (suitable) category $\mathbb{F}$, $TV$ for the
presheaf of terms, $\delta$ for the context extension, and
...
6
votes
3answers
128 views
anonymous lambda functions (functional programming)
What are anonymous (lambda) functions? What is the formal definition of an anonymous function in a functional programming language?
In my simple terms, when I am programming in scheme/lisp I would ...
5
votes
2answers
101 views
Clear, intuitive derivation of the fixed-point combinator (Y combinator)?
The fixed-point combinator FIX (aka the Y combinator) in the (untyped) lambda calculus ($\lambda$) is defined as:
FIX $\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y. ...
1
vote
0answers
119 views
λ-Calculus extensions: meaning of extension symbols
When working with λ-Calculus I see lots of extensions that use other symbols such as
∀ <:Top {} ←, which are from "Types and Programming Languages" (WorldCat) by Benjamin C. Pierce.
...
1
vote
0answers
103 views
Test cases for λ-Calculus
For testing automated theorem provers we have Seventy-Five Problems for Testing
Automatic Theorem Provers by Pelletier.
Are there any such standard/well regarded tests for a λ-calculus that verify ...
3
votes
2answers
113 views
“Applicative order” and “Normal order” in lambda-calculus
Applicative order: Always fully evaluate the arguments of a function
before evaluating the function itself , like -
$(\lambda x. x^2(\lambda x.(x+1) \ \ 2))) \rightarrow (\lambda x.
...
5
votes
3answers
225 views
Can someone give a simple but non-toy example of a context-sensitive grammar?
I'm trying to understand context-sensitive grammars.
I understand why languages like
$\{ww \mid w \in A^*\}$
$\{a^n b^n c^n \mid n\in\mathbb{N}\}$
are not context free, but what I'd ...
7
votes
2answers
149 views
Studying Programming Language Theory
I have recently become extremely interested in understanding and proving aspects of (functional) programming languages.
However as I dive deeper in, things like $\lambda$ calculus, category theory, ...
5
votes
1answer
101 views
Showing the function=? is impossible
Here's a lab from a first-year computer science course, taught in Scheme: https://www.student.cs.uwaterloo.ca/~cs135/assns/a07/a07.pdf
At the end of the lab, it basically presents the halting ...
8
votes
4answers
362 views
Lambda calculus outside functional programming?
I'm a university student, and we're currently studying Lambda Calculus. However, I still have a hard time understanding exactly why this is useful for me. I realize if you do loads of functional ...
3
votes
1answer
49 views
Are two terms where one is without a $\lambda\beta$ normal form unconvertible in $\lambda\beta$?
I know that if you try and make the theory
$$\lambda\beta+\{s = t\ |\text{ s, t are terms without }\lambda\beta\text{ normal forms}\}$$
then that theory becomes inconsistent. Are two terms where one ...
8
votes
1answer
145 views
Concise example of exponential cost of ML type inference
It was brought to my attention that the cost of type inference in a functional language like OCaml can be very high. The claim is that there is a sequence of expressions such that for each expression ...
3
votes
2answers
225 views
Lambda Calculus simplification
Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem.
$$(\lambda mn.(\lambda sz.ms(nsz)))(\lambda sz.sz)(\lambda ...
4
votes
1answer
142 views
Free variables of (λx.xy)x and bound variables of λxy.x
I was solving exercises on Lambda calculus. However, my solutions are different from the answers and I cannot see what is wrong.
Find free variables of $(\lambda x.xy)x$.
My workings: $FV((\lambda ...
8
votes
3answers
181 views
How to show two models of computation are equivalent?
I'm seeking explanation on how one could prove that two models of computation are equivalent. I have been reading books on the subject except that equivalence proofs are omitted. I have a basic idea ...
10
votes
2answers
200 views
$\lambda$-calculus with reflection
I'm looking for a simple calculus that supports reasoning about reflection, namely, the introspection and manipulation of running programs.
Is there an untyped $\lambda$-calculus extension that ...
11
votes
1answer
282 views
Does there exist a Turing complete typed lambda calculus?
Do there exist any Turing complete typed lambda calculi? If so, what are a few examples?
6
votes
2answers
414 views
Representing Negative and Complex Numbers Using Lambda Calculus
Most tutorials on Lambda Calculus provide example where Positive Integers and Booleans can be represented by Functions. What about -1 and i?
7
votes
1answer
160 views
Does High Order Functions provide more power to Functional Programming?
I've asked a similar question on cstheory.SE.
According to this answer on Stackoverflow there is an algorithm that on a non-lazy pure functional programming language has an $\Omega(n \log n)$ ...
5
votes
3answers
203 views
Simple explanation as to why certain computable functions cannot be represented by a typed term?
Reading the paper An Introduction to the Lambda Calculus, I came across a paragraph I didn't really understand, on page 34 (my italics):
Within each of the two paradigms there are several versions ...
9
votes
1answer
137 views
Is there a typed SKI calculus?
Most of us know the correspondence between combinatory logic and lambda calculus. But I've never seen (maybe I haven't looked deep enough) the equivalent of "typed combinators", corresponding to the ...
4
votes
1answer
88 views
Why are lambda-abstractions the only terms that are values in the untyped lambda calculus?
I am confused about the following claim: "The only values in the untyped lambda calculus are lambda-abstractions".
Why are the other terms not values? What does it mean for a lambda-abstraction to be ...
7
votes
1answer
197 views
Reduction rule for IF?
I'm working through Simon Peyton Jones' "The Implementation of Functional Programming Languages" and on page 20 I see:
IF TRUE ((λp.p) 3) ↔ IF TRUE 3 (per β red) (1)
...
4
votes
1answer
262 views
Lambda Calculus beta reduction
I am trying to learn Lambda calculus from here
and while trying to solve some problems, I got stuck. I was trying to solve the following problem (page 14, excercise 2.6 part (i):
Simplify $M \equiv ...
7
votes
1answer
96 views
A lambda calculus evaluation involving Church numerals
I understand that a Church numeral $c_n$ looks like $\lambda s. \lambda z. s$ (... n times ...) $s\;z$. This means nothing more than "the function $s$ applied $n$ times to the function $z$".
A ...
6
votes
1answer
141 views
Lambda Calculus Evaluation
I know this is a simple question but can someone show me how
$(\lambda y. \lambda x. \lambda y.y) (\lambda x. \lambda y. y)$ reduces to $\lambda x. \lambda y. y$.
17
votes
1answer
304 views
Quantum lambda calculus
Classically, there are 3 popular ways to think about computation: Turing machine, circuits, and lambda-calculus (I use this as a catch all for most functional views). All 3 have been fruitful ways to ...
8
votes
3answers
415 views
Is there a difference between $\lambda xy.xy$ and $\lambda x.\lambda y.xy$?
I am currently learning the lambda calculus and was wondering about the following two different kinds of writing a lambda term.
$\lambda xy.xy$
$\lambda x.\lambda y.xy$
Is there any difference ...
8
votes
2answers
259 views
What is beta equivalence?
In the script I am currently reading on the lambda calculus, beta equivalence is defined as this:
The $\beta$-equivalence $\equiv_\beta$ is the smallest equivalence that contains ...
16
votes
2answers
171 views
Characterization of lambda-terms that have union types
Many textbooks cover intersection types in the lambda-calculus. The typing rules for intersection can be defined as follows (on top of the simply typed lambda-calculus with subtyping):
$$
...
