Episode #125 of the Stack Overflow podcast is here. We talk Tilde Club and mechanical keyboards. Listen now

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
73
votes
2answers
7k 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?...
44
votes
2answers
4k 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 ...
34
votes
2answers
2k 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 ...
31
votes
1answer
2k 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?
28
votes
2answers
4k 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 ...
28
votes
2answers
581 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{\...
27
votes
4answers
4k 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. ...
25
votes
1answer
1k 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 ...
22
votes
5answers
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 ...
21
votes
5answers
6k 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 ...
21
votes
0answers
600 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 ...
20
votes
5answers
946 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 ...
20
votes
2answers
2k 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$...
19
votes
1answer
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 ...
18
votes
4answers
914 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 ...
18
votes
2answers
566 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 ...
17
votes
7answers
2k 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 ...
15
votes
3answers
540 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, ...
14
votes
2answers
4k 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?
14
votes
2answers
11k 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))\...
14
votes
1answer
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 ...
14
votes
2answers
1k 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 ...
14
votes
2answers
304 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 ...
13
votes
2answers
1k 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?
13
votes
3answers
1k 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 ...
13
votes
2answers
605 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)$ ...
13
votes
3answers
344 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 ...
13
votes
1answer
219 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 ...
12
votes
2answers
1k 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-...
12
votes
4answers
3k 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 ...
11
votes
3answers
682 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 ...
11
votes
1answer
235 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 ...
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 ...
10
votes
3answers
569 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 ...
10
votes
2answers
241 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," ...
10
votes
2answers
866 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 ...
10
votes
2answers
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 ...
10
votes
1answer
2k 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 ...
10
votes
2answers
1k 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 ...
10
votes
2answers
1k 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 ...
10
votes
2answers
295 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 ...
10
votes
2answers
115 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 ...
10
votes
1answer
488 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 ...
10
votes
1answer
1k views

Algorithm Complexity Analysis on functional programming language implementations

I've learned today that algorithm analysis differs based on computational model. It is something I've never thought about or heard of. An example given to me, that illustrated it further, by User @...
10
votes
1answer
326 views

Do Self Types make the Calculus of Inductive Constructions obsolete?

Self Types are an extension of the Calculus of Constructions [1] that allow the language to express algebraic datatypes encoded through the Scott Encoding. The Scott Encoding provides one the ability ...
10
votes
0answers
308 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 ...
10
votes
0answers
132 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) ...
9
votes
1answer
885 views

λ -calculus : What is the most efficient in memory representation of functions?

I would like to compare performance of function encoded (Church's / Scott's) vs classically encoded (assembler / C) data structures. But before I do that I need to know how efficient is / can be ...
9
votes
1answer
177 views

What is a super universe?

I'm reading this well-known paper On Universes in Type Theory. At first I expected something similar to Setω in Agda, but it turns out that it's even something more ...
9
votes
1answer
271 views

Are combinatory logic terms always larger?

So there is an algorithm to convert lambda calculus terms to combinatory logic using SK combinators. It produces things that explode in size. I would like to know more about this explosion in size. I ...