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

61–70 of 77 posts

Re: Relation Between Type Theory, Category Theory and Logic

#61

Post by gallabytes »

YorkshireSeason wrote: post #28
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…

What is the state of the art of the research on the computational interpretation of univalence? What's working, what's not working? I seem to remember that A Jeffrey said not too long ago that he had a working interpretation.

A lot of work was going into the cubical model, but IIRC they realized it was a dead end about a month and a half ago. Right now the most promising work looks to be formalizing the set theoretic model in NuPRL.

Re: Relation Between Type Theory, Category Theory and Logic

#62

Post by gallabytes »

noreasonw wrote: post #38
igravious wrote: post #24

Earlier quoted context omitted.

Wow. Replying to myself. What is brought into question is the status of Proof by Contradiction, not the status of the Law of Noncontradiction. Russell seems to have confused these two things. And I don't blame him. It was 1940 after all, and there was a war on. Another interesting fact. The book is built up from from accumulated material finally delivered over a course of lectures at Harvard University in a series ca…

Just reading your comment I was thinking about the closed world assumption in logic (prolog), perhaps there are some middle concept between the Proof by Contradiction and the closed world assumption. In the real world we learn concepts (think about relativity or a non planar world) and then the old question is no longer a two value alternative. Perhaps something like: In this field a new conception could appear that…

We have something between the two in HoTT - universes of types is stratified by homotopy levels, corresponding to how many dimensions of structure a type has. A space with only points is thus a 0-type, a space with at most 1 point is a -1-type, and a space with only one is a -2-type.

The catch is that univalence is inconsistent with LEM at h-levels greater than -1, but assuming it is perfectly consistent for -1 types, which can be thought of as the "at most true" propositions of classical logic.

Re: Relation Between Type Theory, Category Theory and Logic

#63

Post by ericbb »

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.

Check out this Scientific American article[1], especially the video of a presentation given by Voevodsky.

Edit: Here's a more direct page[2] if you just want the video.

[1] http://blogs.scientificamerican.com/guest-blog/voevodskye280...

[2] http://www.heidelberg-laureate-forum.org/blog/video/lecture-...

Re: Relation Between Type Theory, Category Theory and Logic

#64

Post by eli_gottlieb »

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)?

No. Homotopy Type Theory is a total language, so even type-level programming simply has to terminate, or the proof-checker won't accept it.

Proving that nontrivially recursive programs terminate can be a bugger.

Re: Relation Between Type Theory, Category Theory and Logic

#65

Post by Kutta »

gallabytes wrote: post #61
YorkshireSeason wrote: post #28

Earlier quoted context omitted.

What is the state of the art of the research on the computational interpretation of univalence? What's working, what's not working? I seem to remember that A Jeffrey said not too long ago that he had a working interpretation.

A lot of work was going into the cubical model, but IIRC they realized it was a dead end about a month and a half ago. Right now the most promising work looks to be formalizing the set theoretic model in NuPRL.

Could you give pointers wrt cubical model being a dead end? As yet I've heard nothing about this.

Re: Relation Between Type Theory, Category Theory and Logic

#66

Post by baddox »

mafribe wrote: post #18
baddox wrote: post #17

Earlier quoted context omitted.

If you limit yourself to only constructive proofs, do you even get the real numbers? I'm not very clear on the definition of "constructive," but given that almost all real numbers are non-computable (i.e. most likely, the set of all real numbers you have ever encountered outside of computability theory has the same cardinality as the integers), it doesn't feel very constructive to me. I've always found it odd that we…

Rest assured that (contrary to j2kun's misleading claims) if some of the world's top mathematicians and computer scientists propose a new foundation of mathematics, they don't forget real numbers. You need to distinguish between non-computable and non-constructive. The proof that the cardinality of the reals is non-countable is perfectly constructive, see [1] for a discussion of these and related issues. [1] https://…

I'm familiar with the diagonal argument, but the version I learned in Discrete Math courses defines the reals as little more than a (potentially infinite) series of digits with a decimal point somewhere, which I thought didn't hold up to much scrutiny. But this stuff is way above my mathematics pay grade. :) I stumbled onto the Wikipedia article "Construction of the real numbers" and I have no clue what is going on.

https://en.wikipedia.org/wiki/Construction_of_the_real_numbe...

Re: Relation Between Type Theory, Category Theory and Logic

#67

Post by jonsterling »

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)?

You do not in general decide whether two types are equivalent. You prove it...

Re: Relation Between Type Theory, Category Theory and Logic

#68

Post by jonsterling »

joe_the_user wrote: post #10
szany wrote: post #7

See also Bob Harper's blog for a more leisurely exposition: https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...

"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…

Bob is coming from the perspective of Brouwerian Intuitionism, and so he is not really that interested in a closed "formal system". So, "proofs" in the setting that Bob cares about are not derivations in a formal system, so Gödel's result doesn't really apply.

Re: Relation Between Type Theory, Category Theory and Logic

#69

Post by cbd1984 »

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…

> The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information).

So strings are equivalent to everything, and vice-versa.

> Now, the issue is that currently we don't actually have a computational interpretation for the univalence axiom

JSON? Sexps?

Re: Relation Between Type Theory, Category Theory and Logic

#70

Post by mafribe »

kazinator wrote: post #51
mafribe wrote: post #16

Earlier quoted context omitted.

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.

    A proof in mathematics is not purely syntactic because it's not purely logical.
This is confusing constructive reasoning with the decision problem for proof validity. They are different things.

The very point of logic, constructive or otherwise, or at least one of the key points for having a logic is to be able to decide whether a given proof object is indeed a valid proof. Valid proofs of course typically also make use of non-logical axioms of the ambient theory. If proof-hood is not decidable, it's not a logic.

Reasoning is constructive if it avoids certain proof principle like LEM (law of excluded middle) or double negation.

Post reply on HN