Skip to main content

# Tag Info

## Hot answers tagged lambda-calculus

43 votes
Accepted

### Why isn't lambda notation popular among mathematicians?

As Derek already said, there is no essential difference between functions $A\times B \to C$ and functions $A\to (B \to C)$ via Currying (this is also more abstractly expressed by the universal ...
• 12.6k
27 votes
Accepted

### The "functions" of untyped lambda calculus are not (set theoretic) functions so what are they?

Actually it is possible to interpret $\lambda$-terms (I assume you use $\lambda$-function as a synonym for $\lambda$-term) as some sort of functions. This is due to a result of Dana Scott, who ...
• 18.3k
18 votes

### The "functions" of untyped lambda calculus are not (set theoretic) functions so what are they?

I've added a section to the bottom of my answer on a more general approach that shows how you can treat functions that can be applied to themselves within set theory, representing them as something ...
• 10.4k
18 votes

### Can someone explain the Y Combinator?

If you know Cantor's diagonal argument, then you can discover the Y combinator. Cantor's Theorem Let $A,B$ be sets and suppose that there exists a fixpoint-free function $f \colon B \to B$. Then there ...
• 25.2k
17 votes

### Function "evaluation" just means "composition"?

That’s right, evaluation is not in any serious way distinct from composition with a function with singleton domain—or to remove all talk of elements entirely, a function whose domain is a terminal ...
• 53.2k
16 votes
Accepted

### Does the Curry-Howard correspondence imply decidibility of natural deduction?

First, the simply typed lambda calculus is actually equivalent to propositional logic, which is decidable. In order to add quantifiers, which boost the power of the calculus to predicate logic (which ...
• 39.1k
15 votes

### Rigorous books on basic computability theory

But is it a good idea to "to avoid as much as possible Church-Turing thesis in my proofs"? Take a book like Cutland's wonderful classic Computability: An Introduction to Recursive Function ...
• 55.6k
14 votes

### Why isn't lambda notation popular among mathematicians?

Lambda calculus is related with computer science through and through. To quote Wikipedia: Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing ...
• 839
13 votes
Accepted

9 votes
Accepted

• 2,738
7 votes
Accepted

### Is lambda calculus a sub-system of first-order logic and set theory?

For theories $T_0$ and $T_1$ over the same language, we say $T_0$ is a subtheory of $T_1$ when every theorem of $T_0$ is also provable in $T_1$. If we require theories are closed under deductions, ...
• 27.7k
6 votes

### Are calculus and real analysis the same thing?

My take on this: One would use the word 'calculus' when one is applying the mathematical tools - chain rule, integration- by-parts, etc - to solve problems in science, engineering, and so on; whereas ...
• 111
6 votes
Accepted

### Unrecognized Quantifiers

The iota ($\iota$) and script A ($\mathcal{A}$) are determiners, not quantifiers in the usual sense; they’re described later, in the slides titled Definite Determiners and Indefinite Determiners. The ...
• 622k
6 votes
Accepted

### Lambda Calculus Grammar

$x(\lambda y.\!y)$ is a perfectly valid lambda term. It's not a closed lambda term, but that is a notion that is usually built on top of this basic notion of lambda terms. (Though, you can directly ...
• 25.3k
6 votes

### Why is it called lambda "calculus"?

This is a good opportunity for using a dictionary. The Oxford dictionary (used in Apple's Dictionary app, which here gives the same result as "calculus" at Oxford Dictionaries online) ...
• 193
6 votes
Accepted

### What is the meaning of this Church numeral example?

The word succ means successor; informally, the successor of a natural number $n \in \mathbb N$ is the natural number $n + 1$. Church numerals are one way to ...
• 27.1k
6 votes
Accepted

• 15.2k
6 votes
Accepted

### Reasoning in natural language vs. reasoning in formal language

This question straddles philosophy and mathematics. Or perhaps I should say, it involves both philosophical and technical questions about mathematics. Also it is ripe with history. On the one hand, ...
• 8,991

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