The type-theory tag has no wiki summary.
23
votes
6answers
2k views
Learning Lambda Calculus
What are some good online/free resources (tutorials, guides, exercises, and the like) for learning Lambda Calculus?
Specifically, I am interested in the following areas:
Untyped lambda calculus
...
10
votes
1answer
468 views
If $f(x)=g(x)$ for all $x:A$, why is it not true that $\lambda x{.}f(x)=\lambda x{.}g(x)$?
There's something about lambda calculus that keeps me puzzled. Suppose we have $x:A\vdash f(x):P(x)$ and $x:A\vdash g(x):P(x)$ for some dependent type $P$ over a type $A$. Then it is not necessarily ...
8
votes
0answers
111 views
Hao Wang's $\mathfrak S$ system: a “transfinite type” theory?
Long ago, while I was reading a book ($*$) about the various way to build set theories (Zermelo-Freankel, Von Neumann–Bernays–Gödel, and type theories), I read about a variant of type theory with ...
6
votes
2answers
335 views
Classic type theory textbooks
There are many classic textbooks in set and category theory (as possible foundations of mathematics), among many others Jech's, Kunen's, and Awodey's.
Are there comparable classic textbooks in ...
6
votes
1answer
277 views
Intuitionistic Banach-Tarski Paradox
While the Banach-Tarski paradox is a counter-intuitive result which requires the Axiom of Choice, leading some people to argue specifically against Choice, and others to argue for constructive ...
6
votes
0answers
167 views
Looking for an approach to mathematical notation wherein the universe is divided into disjoint worlds.
Is there a rigorous approach to mathematical notation wherein the "universe" is divided into disjoint "worlds," and the meaning of notation is world-dependent? This would solve a few pesky problems. ...
5
votes
2answers
335 views
What's the meaning of algebraic data type?
I'm reading a book about Haskell, a programming language, and I came across a construct defined "algebraic data type" that looks like
...
5
votes
2answers
63 views
Is there a theory of extensible definitions?
We can define $+$ as a function $\mathbb{N}^2 \rightarrow \mathbb{N}$, and then prove the theorem:
Thm. The range of $+$ is $\mathbb{N}$.
If we later wish to extend $+$ to a function $\mathbb{Z}^2 ...
4
votes
2answers
69 views
Eilenberg Moore category
I've been trying to code up the Eilenberg-Moore category for a monad in Haskell.
As I understand it, given a category $C$ and a monad $(T,\eta,\mu)$ on $C$ we build the Eilenberg-Moore category $C^T$ ...
4
votes
2answers
118 views
Peano axioms expressed in type theory
I have a very strong understanding of 1st order logic and am trying to lean type theory as an alternative. Could someone express the Peano axioms with type-theory? I am especially interested to see ...
3
votes
2answers
271 views
Curry-Howard correspondence
I read that the Curry-Howard correspondence introduces an isomorphism between typed functions and logical statements. For example, supposedly the function
$$\begin{array}{l}
I : \forall a. a \to a\\
...
3
votes
0answers
41 views
Are large cardinals bi-interperable with type theory?
"Sets in Types, Types in Sets" establishes that the calculus of constructions is bi-interpretable with ZFC + infinitely many inaccessibles.
Are there any more results like this higher up the large ...
2
votes
2answers
212 views
Has a Dependent Type always a Type?
I am experimenting with dependent types. Lets assume the following
short notation:
...
2
votes
1answer
216 views
Constructing dependent product (right adjoint to pullback) in a locally cartesian closed category
I've been trying to find a proof that the pullback functors in a locally cartesian closed category have right adjoints (used to model the notion of indexed product inside a category (rather than ...
2
votes
0answers
60 views
Introductory text about different stratification methods in higher-order logic and set theory
Could someone recommend me a good overview text about stratification of predicates, comprehension axioms, and other methods of avoiding the paradoxes in untyped or only loosely/relatively typed ...
1
vote
2answers
243 views
formal rules for avoiding bound/unbound variable problems in lambda calculus
I have been interested in learning formal math formally enough so that I could write a proof assistant using some simple parsing tools, and explain to someone else with little math knowledge how to ...
1
vote
2answers
132 views
Accessible formal specification and explanation of First Order Logic?
I am trying to get good at proofs by working through How To Prove It. Unfortunately I am very bothered by the fact that I do not understand all the formalities in First Order Logic + set theory ...
1
vote
1answer
28 views
Variables in Types in type theory
I'm slowly grasping this, though the different formulations of type theory make it difficult.
In http://imps.mcmaster.ca/doc/seven-virtues.pdf types can only be formed from *, i, and a->b when a and ...
1
vote
1answer
27 views
in type theory does (x:A) imply ((x:A):A)
In the formulation of type theory I'm reading, (x:A) is an expression of type A. This would seem to imply ((x:A):A) and (((x:A):A):A)... Is this a common feature of type theories? Or am I reading too ...
1
vote
2answers
28 views
mapping simple first oreder problems to type theory
Since Peano axioms expressed in type theory doesn't seem to be going anywhere, here is a simpler question:
How would I map simple first order systems to an equivalent type theoretic notation.
...
1
vote
0answers
39 views
How does type theory handle division by zero and such?
Say I have a program that needs to not divide by zero:
f(x):
if nonzero(x):
return sin(x)/x
else:
return 1
If we divide by zero, we get ...
1
vote
0answers
26 views
Enumeration of symbols in grammatical expressions or vertices in tree graphs
I have expressions (type of a function) like e.g.
$$f:(A\to B)\to C \to (D\to E)\to F.$$
(Where I understand $A\to B\to C$ as $A\to (B\to C)$, in case that is relevant.)
There might be information ...
0
votes
1answer
56 views
Natural numbers as types.
My question could be simple but I haven't found an answer for it: could we define a type theory where the types are the natural numbers themselves (not the set of the natural numbers)?
Thanks.
-1
votes
1answer
166 views
How to understand inductive definitions of recursive data types?
The problem was encountered when learning Computability Notes by Roberto Zunino (link), page 9 and 11. It seems as if it is a well-known issue and I don't need to specify the "canonical" meaning of ...
