Skip to main content

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
79 votes
2 answers
8k views

What does the "Lambda" in "Lambda calculus" stand for?

I've been reading about Lambda calculus recently but strangely I can't find an explanation for why it is called "Lambda" or where the expression comes from. Can anyone explain the origins of the term?...
Klangen's user avatar
  • 1,100
47 votes
2 answers
6k views

How does the Y combinator exemplify "Lambda calculus inconsistency"?

On the Wikipedia page for Fixed Point Combinators is written the rather mysterious text The Y combinator is an example of what makes the Lambda calculus inconsistent. So it should be regarded with ...
Ben I.'s user avatar
  • 1,710
37 votes
2 answers
3k 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 ...
Artem Kaznatcheev's user avatar
36 votes
7 answers
7k 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. ...
BlueBomber's user avatar
  • 1,297
32 votes
1 answer
3k 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?
Snowball's user avatar
  • 423
30 votes
2 answers
5k views

Is Lambda Calculus purely syntactic?

I've been reading for a few weeks about the Lambda Calculus, but I have not yet seen anything that is materially distinct from existing mathematical functions, and I want to know whether it is just a ...
Neil's user avatar
  • 431
30 votes
3 answers
871 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): $$ \dfrac{\...
Gilles 'SO- stop being evil''s user avatar
29 votes
5 answers
10k views

Why are functional languages Turing complete?

Perhaps my limited understanding of the subject is incorrect, but this is what I understand so far: Functional programming is based off of Lambda Calculus, formulated by Alonzo Church. Imperative ...
Honinbo Shusaku's user avatar
27 votes
1 answer
2k 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 ...
Hugo Sereno Ferreira's user avatar
25 votes
5 answers
1k 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 ...
Dave Clarke's user avatar
  • 20.2k
24 votes
2 answers
4k 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 $\rightarrow_\beta$...
magnattic's user avatar
  • 547
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,137
22 votes
2 answers
1k views

Basis sets for combinator calculus

It is well known that the S and K combinators form a basis set for combinator calculus, in the sense that all other combinators can be expressed in terms of them. There is also Curry's B, C, K, W ...
N. Virgo's user avatar
  • 976
21 votes
5 answers
1k 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 ...
Jacob's user avatar
  • 313
20 votes
4 answers
1k views

Why is it important for functions to be anonymous in lambda calculus?

I was watching the lecture by Jim Weirich, titled 'Adventures in Functional Programming'. In this lecture, he introduces the concept of Y-combinators, which essentially finds the fixed point for ...
Rohan Prabhu's user avatar
20 votes
7 answers
3k views

Lambda calculus didn't seem abstract. And I can't see the point of it

The underlying question: What does lambda calculus do for us that we can't do with the basic function properties and notation generally learned in middle school algebra? First of all, what does ...
JDG's user avatar
  • 353
20 votes
1 answer
2k views

if (λ x . x x) has a type, then is the type system inconsistent?

If a type system can assign a type to λ x . x x, or to the non-terminating (λx . x x) (λ x . x x), then is that system ...
MaiaVictor's user avatar
  • 4,137
17 votes
2 answers
14k 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. x^2(2+1))\...
URL87's user avatar
  • 755
17 votes
3 answers
841 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, ...
daniel gratzer's user avatar
16 votes
3 answers
2k views

A quine in pure lambda calculus

I would like an example of a quine in pure lambda calculus. I was quite surprised that I couldn't find one by googling. The quine page lists quines for many "real" languages, but not for lambda ...
N. Virgo's user avatar
  • 976
15 votes
4 answers
5k 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 like ...
BlueBomber's user avatar
  • 1,297
15 votes
2 answers
451 views

Is the SK2 calculus a complete basis, where K2 is the flipped K combinator?

Specifically, if I defined a new $K_2$ as $$K_2 = \lambda x. (\lambda y. y)$$ instead of $$K = \lambda x. (\lambda y. x)$$ would the $\{S, K_2,I\}$-calculus be a compete basis? My guess is "no," ...
cole's user avatar
  • 253
14 votes
2 answers
7k 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?
zcaudate's user avatar
  • 273
14 votes
1 answer
2k views

Why will the Hindley-Milner algorithm never yield a type like t1 -> t2?

I'm reading about the Hindley-Milner typing algorithm while writing an implementation, and see that, as long as every variable is bound, you'll always get either atomic types or types where the ...
Juan's user avatar
  • 765
14 votes
1 answer
3k 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 ...
mrrusof's user avatar
  • 241
14 votes
2 answers
2k views

Solving functional equations for unknown functions in lambda calculus

Are there any techniques for solving functional equations for unknown functions in lambda calculus? Suppose I have the identity function defined extensionally as such: $I x = x$ (that is, by ...
BarbaraKwarc's user avatar
14 votes
3 answers
597 views

What's the difference between a calculus and a programming language?

I think I'm pretty confused about what's called a calculus and what's called a programming language. I tend to think, and might have been told, that a calculus is a formal system for reasoning about ...
Guido's user avatar
  • 398
14 votes
2 answers
368 views

Are there peer-reviewed papers studying the pros and cons of functional programming?

Can somebody refer me to peer-reviewed papers studying the advantages or disadvantages of writing code in a functional style? Are there papers which discuss the applications of Lambda Calculus in ...
Dokkat's user avatar
  • 149
14 votes
0 answers
2k views

Barendregt's Variable Convention: what does it mean?

Barendregt's Variable Convention: If $M_1,...,M_n$ occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free ...
alim's user avatar
  • 1,014
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
13 votes
2 answers
2k views

Lambda calculus: difference between contexts and evaluation contexts

Firstly, I'd like to say that my text below may contain errors, so feel free to point out any mistakes in my formulation of the question. Consider an untyped lambda calculus with booleans and if-...
user avatar
13 votes
2 answers
2k views

Is there a theory/abstraction behind OOP?

Functional programming has the very elegant Lambda Calculus and its variants as a backup theory. Is there such a thing for OOP? What is an abstraction for the object oriented model?
Viclib's user avatar
  • 441
13 votes
1 answer
26k views

Difference between normal-order and applicative-order evaluation

The language I'm learning is Scheme and I'm working on an exercise that gives this: ...
user224530's user avatar
13 votes
2 answers
824 views

Do Higher 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)$ ...
vz0's user avatar
  • 233
13 votes
1 answer
281 views

What functions can combinator calculus expressions compute?

A combinator expression (let's say in the SK basis) can be thought of as a function that maps combinator calculus expressions to combinator calculus expressions. That is, one can think of an ...
N. Virgo's user avatar
  • 976
12 votes
1 answer
447 views

What is $Prop$ in the calculus of constructions?

I'm looking at the Calculus of Constructions and its place in the Lambda Cube. If I understand correctly, each axis of the cube can be thought of as adding another operation involving types to the ...
Michael Rawson's user avatar
12 votes
1 answer
734 views

Simplest complete combinator basis pair for flat expressions

In Chris Okasaki's paper "Flattening Combinators: Surviving Without Parentheses" he shows that two combinators are both sufficient and necessary as a basis to encode Turing-complete expressions ...
user avatar
11 votes
3 answers
1k 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 in ...
magnattic's user avatar
  • 547
11 votes
2 answers
1k views

Universal/existential quantification?

I'm struggling to understand the purpose of universal and existential quantification of types. I'm playing around with writing a toy language based on the calculus of constructions. I've been reading ...
oconnor0's user avatar
  • 393
11 votes
2 answers
2k views

Define a list using only the Hindley-Milner type system

I'm working on a small lambda calculus compiler that has a working Hindley-Milner type inference system and now also supports recursive let's (not in the linked code), which I understand should be ...
Juan's user avatar
  • 765
11 votes
2 answers
2k views

Is there an equivalent of lambda calculus for object oriented languages? [duplicate]

Lambda calculus serves as a foundation for all sorts of functional languages and its various extensions are compiler targets for languages like Haskell, ML, etc. So what is the equivalent for object ...
user avatar
11 votes
0 answers
872 views

Advantages of algorithm W over algorithm J for type inference in Hindley-Milner type system

According to A modern eye on ML type inference Furthermore, for some unknown reason, W appears to have become more popular than J, even though the latter is viewed—with reason!—by Milner as ...
Alexey Romanov's user avatar
11 votes
0 answers
207 views

When can you "invert" an equation in the lambda calculus

Suppose that $M$ is a full model of the simply typed lambda calculus. Suppose each base type is infinite. Now suppose that $f$ and $g$ are two functions in $M$ (not necessarily in the same domain) ...
Andrew Bacon's user avatar
10 votes
4 answers
4k views

What are some interesting/important Programming Language Concepts I could teach myself in the coming semester?

I’m a CS senior with and Individual Study period this coming semester, and I’ve decided I’d like to learn more about Programming Language Concepts. More specifically, different programming paradigms, ...
swr52's user avatar
  • 119
10 votes
3 answers
725 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 ...
CodeKingPlusPlus's user avatar
10 votes
2 answers
2k views

What makes lambda calculus relevant to study?

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 ...
Jules's user avatar
  • 632
10 votes
1 answer
2k views

What is the difference between the Mogensen-Scott and the Boehm-Berarducci encoding for ADTs on the Lambda Calculus?

On the Lambda Calculus, there are several different ways to represent a list. For example, one can encode it as its right fold: ...
MaiaVictor's user avatar
  • 4,137
10 votes
2 answers
413 views

Combinatory interpretation of lambda calculus

According to Peter Selinger, The Lambda Calculus is Algebraic (PDF). Early in this article he says: The combinatory interpretation of the lambda calculus is known to be imperfect, because it does ...
sshine's user avatar
  • 519
10 votes
2 answers
358 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
10 votes
1 answer
627 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 ...
codd's user avatar
  • 701

1
2 3 4 5
12