Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Relation Between Type Theory, Category Theory and Logic

ncatlab.org

Post reply on HN
Print view View original

51–60 of 77 posts

Re: Relation Between Type Theory, Category Theory and Logic

#51

Post by kazinator »

mafribe wrote: post #16
j2kun wrote: post #13

Earlier quoted context omitted.

I'll try to keep it short and skip the details of the mathematical framework itself. Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not…

j2kun's characterisation of HoTT is misleading. Their goal is also to rewrite all of mathematics in a constructive way, This is not the goal of HoTT, and also not possible as some mathematics is intrinsically non-constructive. HoTT allows non-constructive reasoning, see section 3.4 "Classical vs. intuitionistic logic" of the HoTT book http://homotopytypetheory.org/book/ . You can say that HoTT derives non-constructiv…

A proof in mathematics is not purely syntactic because it's not purely logical. For instance, in some steps of a proof, we do something to both sides of an equation and argue that it is still balanced, based on rules that are outside of logic. Such a step can have a nonconstructive element.

Re: Relation Between Type Theory, Category Theory and Logic

#52

Post by igravious »

IngoBlechschmid wrote: post #47
igravious wrote: post #42

Earlier quoted context omitted.

You melted my brain. What does “quantify over all formulas” mean? From the way you state it, that's an interesting perspective. But it seems to be from a perspective of totality which I'm wary of. Not saying you're wrong, going to check out those links. Andrej Bauer was very kind to answer an out-of-the-blue email query of mine once :) Seriously appreciative of your response, a thousand thanks! EDIT: Ok, I've read yo…

Sorry, didn't intend to use so much jargon. By "quantifying over all formulas" I just meant that one has to distinguish between the following two statements: 1. The law of excluded middle holds for a particular formula p. 2. The law of excluded middle holds for _all_ formulas p. Also note that "formula" just means "formal logical statement", i.e. structured string consisting of v, ==>, and so on. What do you mean by…

I too would be glad, it's been enlightening already. We have common interests it seems :)

By structured string you mean well-formed formula I guess.

"perspective of totality" means taking all `things' together at once (if that were possible)

Re: Relation Between Type Theory, Category Theory and Logic

#53

Post by jules »

YorkshireSeason wrote: post #36
jules wrote: post #34

Earlier quoted context omitted.

I wouldn't call that a proper treatment of equality. It is unsatisfactory in several ways: no proper equality on functions (function extensionality), no proper equality on types (univalence), no quotient types (~= HITs), and since refl is the only proof of equality it doesn't even make much sense to talk about equality on equalities. More fundamentally the idea that refl is the only proof of equality just doesn't sit…

This discussion goes way beyond an "absolute layman explanation to homotopy type theory" ... Anyway, I disagree that the "whole idea of type theory is that things can have more than one proof". UIP is about identity types and their proofs. Identity types are very special types. It is far from obvious that they should be inhabited by more than one proof. Indeed, it was a surprising breakthrough when Streicher/Hoffmann…

It's true that it was a discovery that Martin Lof identity types could have multiple inhabitants, but it's a general principle of type theory that types can have multiple inhabitants (unlike in set theory, where propositions are just true). That this also applies to identity types in HoTT is a sign that something is going right.

Furthermore, from another perspective it's "obvious" that identity types should have multiple inhabitants. There were two approaches to equality in type theory. One is Martin Lof identity types, which follow naturally from Leibniz' principle that A and B are equal then they are indistinguishable. The other is defining equality for each type on a case by case basis (pairs are equal if their components are equal, functions are equal if they give equal outputs, etc.), like in section 2.4 Equality of this paper: http://www.andres-loeh.de/PiSigma/PiSigma.pdf

In the latter approach it's obvious that equality has multiple inhabitants, because it's defined that way. For example we can define equality of unordered pairs as the type:

    id_unordered_pair : (A,A) -> (A,A) -> Type
    id_unordered_pair (a,b) (c,d) = (id_A a c)*(id_A b d) + (id_A a d)*(id_A b c)
i.e. two unordered pairs (a,b) and (c,d) are equal if a=c and b=d or a=d and b=c.

This has two inhabitants even if id_A has only a single inhabitant. This approach naturally accommodates quotient types. The problem with it is that the type system has no idea that this is equality. It's just another definition. The point of equality is that all functions respect equality (equal inputs to equal outputs). Not all functions respect equality on these unordered pairs (e.g. a function that extracts the first component).

This approach to equality has the converse of Leibniz' rule: we can define equality so that if two things are indistinguishable then they are equal.

I think a good view of HoTT is as unifying these two approaches to equality. We get both Leibniz' principle and its converse, and we get user defined equality types whose equality is respected by all functions, we get multiple inhabitants for equality types.

Re: Relation Between Type Theory, Category Theory and Logic

#54

Post by jules »

tmvphil wrote: post #45
Kutta wrote: post #25

Earlier quoted context omitted.

Another addendum to the discussion, from an angle more relevant to computer programmers: if we find a computational meaning for the univalence axiom, then it'll be a crazy nuclear weapon of generic programming and code generation. The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information). For example, one Boolean type may be defined as an enum conta…

I must be missing something. A proof that Bool and Bool2 are equal is a bijection f :: Bool -> Bool2. So given any g :: Bool -> Bool we have (f . g . f^-1) :: Bool2 -> Bool2. So it seems trivial.

Yes, that's pretty much it. Doing this systematically for all types including dependent types that quantify over Bool, as well as for user defined higher inductive types is another matter.

Re: Relation Between Type Theory, Category Theory and Logic

#55

Post by Kutta »

tmvphil wrote: post #45
Kutta wrote: post #25

Earlier quoted context omitted.

Another addendum to the discussion, from an angle more relevant to computer programmers: if we find a computational meaning for the univalence axiom, then it'll be a crazy nuclear weapon of generic programming and code generation. The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information). For example, one Boolean type may be defined as an enum conta…

I must be missing something. A proof that Bool and Bool2 are equal is a bijection f :: Bool -> Bool2. So given any g :: Bool -> Bool we have (f . g . f^-1) :: Bool2 -> Bool2. So it seems trivial.

A more interesting example: substitute natural numbers with binary trees. After all, they're equivalent. Now univalence would have to implement the binary tree analogue for every function on naturals, in a way that preserves semantics with respect to our conversion function.

Re: Relation Between Type Theory, Category Theory and Logic

#56

Post by joe_the_user »

mafribe wrote: post #19
joe_the_user wrote: post #10

Earlier quoted context omitted.

"Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!" The thing I never understood about statements of this sort is that in my understanding of model theory, Godel's theorem and so-forth, a proof is a rare thing. Most of the true statements in a given model don't have proofs. Any consistent proof…

While Goedel's first incompleteness theorem indeed shows that there will always be true statements that don't follow from a given set of (computable) axioms, this is almost never a problem in practise. It is hard to find natural examples of such statements. Almost every mathematical statement (or its negation) you or I can come up with is a consequence of the axioms of ZFC set theory, or whatever other foundation you…

It doesn't follow in normal mathematical practice I think because mathematicians want natural, sane axioms that lead to human understandable models.

Computing already starts out much messier in its activities. Determining what will happen when a large system gets input is tricky.

I'm not sure what could proved about the operations of a "deep neural net" for example.

Re: Relation Between Type Theory, Category Theory and Logic

#57

Post by rndn »

Kutta wrote: post #25
Xcelerate wrote: post #8

Can someone give me an absolute layman explanation to homotopy type theory (and why it's so interesting)? I'm hearing about it everywhere, but most of the introductions to the subject assume the reader is already familiar with either type theory or category theory.

Another addendum to the discussion, from an angle more relevant to computer programmers: if we find a computational meaning for the univalence axiom, then it'll be a crazy nuclear weapon of generic programming and code generation. The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information). For example, one Boolean type may be defined as an enum conta…

Doesn't the halting problem pose an obstacle in deciding whether two types act in an equivalent way (similar to how the equivalence between two programs is undecidable)?

Re: Relation Between Type Theory, Category Theory and Logic

#58

Post by solomatov »

Xcelerate wrote: post #8

Can someone give me an absolute layman explanation to homotopy type theory (and why it's so interesting)? I'm hearing about it everywhere, but most of the introductions to the subject assume the reader is already familiar with either type theory or category theory.

Homotopy type theory formalizes informal reasoning style when things which have "the same structure" are considered equal in a constructive type theory setting. Another achievement is formulation of synthetic homotopy type theory, i.e. axiomatic as opposed to based on geometric type theory.

Re: Relation Between Type Theory, Category Theory and Logic

#60

Post by gallabytes »

rndn wrote: post #57
Kutta wrote: post #25

Earlier quoted context omitted.

Another addendum to the discussion, from an angle more relevant to computer programmers: if we find a computational meaning for the univalence axiom, then it'll be a crazy nuclear weapon of generic programming and code generation. The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information). For example, one Boolean type may be defined as an enum conta…

Doesn't the halting problem pose an obstacle in deciding whether two types act in an equivalent way (similar to how the equivalence between two programs is undecidable)?

Why would it do that? Univalence is unrelated to the halting problem.

What the univalence axiom says is that you can treat types you have proven isomorphic as equal.

Post reply on HN