2022 Developer Survey is open! Take survey.
85 votes
Accepted

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

An excerpt from History of Lambda-calculus and Combinatory Logic by F. Cardone and J.R. Hindley(2006): By the way, why did Church choose the notation “$\lambda$”? In [Church, 1964, §2] he stated ...
user avatar
  • 3,419
64 votes
Accepted

Is Lambda Calculus purely syntactic?

Ironically, the title is on point but not in the way you seem to mean it which is "is the lambda calculus just a notational convention" which is not accurate. Lambda terms are not functions1. They ...
user avatar
51 votes
Accepted

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

It's inspired from real events, but the way it's stated is barely recognizable and “should be regarded with suspicion” is nonsense. Consistency has a precise meaning in logic: a consistent theory is ...
user avatar
31 votes
Accepted

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

Very good explanations of programming paradigms and the programming concepts from which those paradigms are built are found in Peter van Roy's works. Especially in the book Concepts, Techniques, and ...
user avatar
29 votes
Accepted

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

The main theorem regarding this issue is due to a British mathematician from the end of the 16th century, called William Shakespeare. His best known paper on the subject is entitled "Romeo and Juliet" ...
user avatar
  • 19.1k
29 votes
Accepted

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

Certainly, assigning a type to $\lambda x. x\ x$ is not enough for inconsistency: in system $F$, we can derive $$ \lambda x.x\ x:(\forall X.X)\rightarrow (\forall X.X)$$ in a pretty straightforward ...
user avatar
  • 7,744
25 votes
Accepted

Why are functional languages Turing complete?

In a nutshell: What characterizes imperative programming languages as close to Turing machines and to usual computers such as PCs, (themselves closer to random access machines (RAM) rather than to ...
user avatar
  • 19.1k
24 votes
Accepted

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

There are many reasons why the lambda calculus is so important. A very important reason is the lambda calculus allows us to have a model of computation in which computable functions are first-class ...
user avatar
  • 2,418
24 votes
Accepted

Lambda Calculus Generator

Sure, this is a standard encoding exercise. First of all, let $p : \mathbb N^2 \to \mathbb N$ any bijective computable function, called a pairing function. A standard choice is $$ p(n,m) = \dfrac{(n+m)...
user avatar
  • 14.1k
23 votes

Difference between normal-order and applicative-order evaluation

What research have you done to answer that question? I just plugged it as it is in Google, and got as second answer (the first may be as good, I did not check) a reference to a section of a bible on ...
user avatar
  • 19.1k
23 votes

Why are functional languages Turing complete?

Turing-complete is just a name. You can call it Abdul-complete if you want. Names are decided upon historically and are often named after the "wrong" people. It's a sociological process that has no ...
user avatar
18 votes
Accepted

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

Consider the terms of the $S,K_2,I$ calculus as trees (with binary nodes representing applications, and $S, K_2$ leaves representing the combinators. For example, the term $S(SS)K_2$ would be ...
user avatar
  • 355
16 votes
Accepted

What is $Prop$ in the calculus of constructions?

In traditional Martin-Löf type theory there is no distinction between types and propositions. This goes under the slogan "propositions as types". But there are sometimes reasons for distinguishing ...
user avatar
  • 28.1k
15 votes

Lambda calculus: difference between contexts and evaluation contexts

A context is a syntactic notion. A context is a term with one hole in it. (Occasionally there are multi-hole contexts, the definition will be given clearly in that case.) The syntax of contexts is ...
user avatar
15 votes

Lambda calculus: difference between contexts and evaluation contexts

Context are used for many purposes, but typically to define congruences on programs. Evaluation contexts are a subset of contexts. They are typically used to define reduction relations. Let me give an ...
user avatar
14 votes

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

So what is the equivalent for object oriented languages? Lambda calculus. I mean, there is Cardelli's object calculus (and a handful of derivatives), but in general, there's nothing fancy about ...
user avatar
  • 499
13 votes

Solving functional equations for unknown functions in lambda calculus

This is a known problem, known as Higher Order Unification. Unfortunately, this problem is undecidable in general. There is a decidable fragment, known as Miller's Pattern Fragment. It's used ...
user avatar
  • 29.1k
13 votes

Lambda Calculus Generator

As has been mentioned, this is just enumerating terms from a context free language, so definitely doable. But there's more interesting math behind it, going into the field of analytical combinatorics....
user avatar
12 votes

Quantum lambda calculus

Apologies in advance for the shameless plug, but there is a paper of mine on a quantum lambda calculus that you may find interesting. It is called The Dagger Lambda Calculus and provides a higher-...
user avatar
12 votes

Is there a theory/abstraction behind OOP?

The connection between object model core and set theory is described in the following documents: Object Membership: The Core Structure of Object Technology Object Membership – Basic Structure What Is ...
user avatar
  • 227
12 votes

Why are functional languages Turing complete?

Because "Turing-complete" just means "it can compute whatever a Turing machine can compute."
user avatar
12 votes

Is there an algorithm for converting Turing machines into equivalent Lambda expressions?

All proofs of the equivalence of these two models of computation are constructive, that is they describe an algorithm for converting a program from one model of computation to the other. However, I ...
user avatar
12 votes
Accepted

Universal/existential quantification?

It helps to remember that $\forall$ (or $\Pi$ as you sometimes see) is a type. It's generalizing $\to$. So while it makes perfect sense to say $(\lambda x : A. M)\ N$, it doesn't make sense to say $(\...
user avatar
12 votes

Lambda Calculus Generator

Yes. Take something that enumerates all possible ASCII strings. For each output, check if it is a valid lambda calculus syntax that defines a function; if not, skip it. (That check can be done.) ...
user avatar
  • 140k
11 votes

What is the purpose of the SKI combinator calculus(or even lambda calculus)? What are some real life examples of its use?

The obvious application of the lambda calculus is any functional programming language (e.g., Lisp, ML, Haskell), and any language that supports anonymous functions. As for combinator calculus, does ...
user avatar
11 votes
Accepted

What is a super universe?

One intention behind having a universe operator and a super-universe closed under it, is to give a type-theoretic version of large cardinal axioms known from set theory. An inaccessible cardinal is ...
user avatar
  • 28.1k
11 votes
Accepted

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

The thing is, there's really not much leeway in terms of function encoding. Here are the main options: Term rewriting: you store functions as their abstract syntax trees (or some encoding thereof. ...
user avatar
  • 29.1k
11 votes
Accepted

$\lambda$-calculus, is there encoding of for or while?

Sure! Let me show how to encode FOR using an example. Suppose we want to translate a simple factorial FOR program x := 1 for i := 1 to N do x := x * i We ...
user avatar
  • 14.1k
10 votes

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

I would like to venture an opinion that is different from those of @babou and @YuvalFilmus: It is vital for pure $\lambda$-calculus to have anonymous functions. The problem with having only named ...
user avatar
10 votes
Accepted

A quine in pure lambda calculus

You want a term $Q$ such that $\forall M \in \Lambda$: $$QM \rhd_\beta Q$$ I will specify no further restrictions on $Q$ (e.g. regarding its form and whether it is normalising) and I will show you ...
user avatar
  • 576

Only top scored, non community-wiki answers of a minimum length are eligible