The type-theory tag has no wiki summary.
2
votes
0answers
11 views
Do any authors takes structures and objects as mutually exclusive concepts?
Having learned that
(link) it's not always obvious to which category a structure should belong, and
(link) the objects of distinct categories are best viewed as disjoint (which makes it very ...
1
vote
1answer
22 views
Is there some sort of function transformation expressing $(X\implies Y)\Leftrightarrow (\neg X\lor Y)$?
Is there a functional interpretation if the replacement for for the material implication?:
$$(X\implies Y)\Leftrightarrow (\neg X\lor Y)$$
Given a function from type $X$ to type $Y$, viewed as a ...
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 ...
8
votes
0answers
113 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 ...
3
votes
0answers
43 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 ...
1
vote
1answer
29 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
29 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.
...
6
votes
0answers
169 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. ...
4
votes
2answers
120 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 ...
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 ...
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$ ...
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
59 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 ...
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 ...
3
votes
2answers
276 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\\
...
10
votes
1answer
469 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 ...
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 ...
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
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 ...
2
votes
1answer
218 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 ...
5
votes
2answers
337 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
...
1
vote
2answers
133 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
2answers
244 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 ...
24
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
...
