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
Function "evaluation" just means "composition"?
Basically, yes, what you are saying is that in the category of sets and functions the action of composition of $f\colon A\to B$ with $(a)\colon \star \to A$ is precisely encoding function evaluation $...
- 80.6k
13
votes
Rigorous books on basic computability theory
Well, arguably the best way to do it completely rigorously would be to first set up a simple programming language L that supports:
String variables (binary strings suffice).
Basic string manipulation:...
- 59.5k
11
votes
I'm probably wrong about Curry-Howard
Your reasoning is right. Unlike untyped lambda calculus, simply typed lambda calculus is strongly normalizing. And unlike untyped lambda calculus, simply typed lambda calculus is not Turing complete.
- 61.1k
9
votes
Accepted
Lambda Calculus factorial
If we exploit the iteration that we get for free from the Church numerals, we don't need to do our own fixpoints, so we can get through a lot easier than DanielV's solution.
If we create a function $...
9
votes
Accepted
Syntactic proof that Peirce's law doesn't hold in simply-typed lambda calculus
You are right in your intuition that proving that a derivation does not exist is somewhat cumbersome. Soundness and completeness of formal proof systems provide us with an interesting duality:
$\vDash ...
- 10.7k
8
votes
Accepted
"Recursive types for free!" -- But doesn't this contradict the fact that $\mathbb{N} \notin \mathbf{FinSet}$?
I am not sure what is the source of confusion here exactly, so let me note some things:
First, the following two statements are not contradictory
A type theory has an infinite type, i.e. a type with ...
- 1,175
7
votes
Why is lambda calculus named after that specific Greek letter? Why not “rho calculus”, for example?
Dana Scott, who was a PhD student of Church, addressed this question. He said that, in Church's words, the reasoning was "eeny, meeny, miny, moe" — in other words, an arbitrary choice for no reason. ...
- 171
7
votes
Accepted
Y combinator as an application of Lawvere's fixed point theorem
What Scott did with domain theory was construct a cartesian closed category with $\varphi:D\cong D^D$. More generally, we have an retraction, i.e. split epimorphism, $D\to D^D$. Isomorphisms/split-...
- 25.3k
7
votes
What axioms can be added to $S,K$ combinator algebra without making it collapse into triviality?
In general, the answer is essentially negative, because of Böhm's separability theorem. This a fundamental result in the theory of the $\lambda$-calculus and combinatory logic. For an informal but ...
- 17.4k
7
votes
Accepted
(How) does lambda calculus encode/use associativity of function composition?
In general it is not the case that given lambda terms $f,g,h$, then $(fg)h = f(gh)$. For example, let $I=\lambda x.x$, and take
$$f =\lambda x.\lambda y.x,\quad g=h = I$$
then $(fg)h = I$, however $f(...
- 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
Are there recursive types in the theory of simple types? If not, how do I prove it?
We can inductively define a function $n \colon \mathbb T \to \mathbb N$ counting the number of arrows of a simple type as follows:
If $\alpha \in \mathbb V$, then $n(\alpha) = 0$.
If $\sigma, \tau \...
- 6,893
6
votes
Accepted
Lambda calculus substitution rule explanation
The question is subtle.
First, $[x \mapsto s]y$ stands for the term obtained from $y$ by replacing $x$ with $s$. So, I'm not a native English speaker but I would say that you are substituting $s$ for ...
- 17.4k
6
votes
Where and how lambda calculus is used?
I highly disagree that the lambda calculus is too abstract and theoretical. The lambda calculus is far simpler than any other model of computation I know of. The only concept needed to understand what'...
- 32.3k
6
votes
How exactly is lambda calculus the foundation for functional programming languages?
Welcome to MSE!
Lambda Calculus is horribly inefficient for modern computers, and so every programming language meant for use in the real world (this category includes both Haskell and Lisp) has a lot ...
- 39.1k
6
votes
Accepted
Why is $\lambda x.\lambda y.xy$ not reducible to $\lambda x.x$?
'Normal form' typically means '$\beta$ normal form' and not '$\beta\eta$ normal form', so your $\eta$-reduction step is not allowed by the normal form calculators.
- 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