3 ms·

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

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-graphic.jpg https://zmichaelgehlke.com/images/curry-howard-square-graphi...

082349872349872 4y ago
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 https://www.cs.bham.ac.uk/~sjv/talks.php
- zmgsabst 4y 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-images https://www.zmgsabstract.com/whitepapers/shapes-as-digital-i... https://www.zmgsabstract.com/whitepapers/shapes-have-operations 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.
  - 082349872349872 4y ago
    Cool! Feel free to let me know when you've written up groups/Zn.

082349872349872 4y ago

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 https://www.cs.bham.ac.uk/~sjv/talks.php

zmgsabst 4y 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-images https://www.zmgsabstract.com/whitepapers/shapes-as-digital-i... https://www.zmgsabstract.com/whitepapers/shapes-have-operations 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.
- 082349872349872 4y ago
  Cool! Feel free to let me know when you've written up groups/Zn.