undefined | Better HN

0 pointszmgsabst3y ago0 comments

You have something like this [1], where you have clear maps from the type theory world into the typed representation of software and the category map structures to Euclidean VM/difference EQ representation of software. This is classic Curry-Howard.

And algebra/geometry split of being/becoming happens in both the type theory/category theory and typed program/difference equation relations.

[1] - https://zmichaelgehlke.com/images/curry-howard-square-graphi...

0 comments

3 comments · 1 top-level

0823498723498723y ago· 2 in thread

could I get a quick example? let's say the top of the square is:

    A * A->B                 
    --------     <------>    f(x), where f:A->B and x:A
       B

what does that interval map onto on the bottom of the square? is the inverse map also interesting?

Edit: are you familiar with Vicker's work? if so, would it help understand (I have it saved off but have not gotten into it yet) the content of the square? https://www.cs.bham.ac.uk/~sjv/talks.php

zmgsabstOP3y ago

I have two white papers on transporting shape types to difference equations on images; and am working on a third related to models of Zn.

https://www.zmgsabstract.com/whitepapers/shapes-as-digital-i...

https://www.zmgsabstract.com/whitepapers/shapes-have-operati...

This is pretty new; but the main interest is actually the inverse mapping — can you recover a type theory that is the “internal language” of the diagram modeling the difference equations that (eg) represents a DNN?

That would be the “effective semantics” of the DNN, expressed as typed statements.

- - -

I’m following the work of (eg) Michael Shulman on attaching types to categories; and my own experience as an SDE on the logic, types, difference equation side. (There’s some papers on programs as Euclidean VMs I used as well, but I don’t have them handy.)

The weakest link is category to difference equations; but that exists to some degree already due to physics — and I’m muddling my way through implementing that to gain deeper insight myself.

0823498723498723y ago

Cool! Feel free to let me know when you've written up groups/Zn.

j / k navigate · click thread line to collapse