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.

401 questions
Filter by
Sorted by
Tagged with
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?...
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 ...
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 ...
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?
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 ...
581 views

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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 @...
326 views

Do Self Types make the Calculus of Inductive Constructions obsolete?

Self Types are an extension of the Calculus of Constructions  that allow the language to express algebraic datatypes encoded through the Scott Encoding. The Scott Encoding provides one the ability ...
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 ...
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) ...
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 ...