search

jonsterling / JonPRL

An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]
http://www.jonprl.org
MIT License
109 stars 9 forks source link

Formalize domain theory #93

Open ghost opened 9 years ago

ghost commented 9 years ago

Someday it would nice to use JonPRL to reason about synthetic topology, eventually with applications to higher-dimensional groupoids and abstract stone duality. But before that, we need some basic domain theory in place first. I think a good source to use would be Escardó/Ho' paper: Operational domain theory and topology of sequential programming languages

jonsterling commented 9 years ago

I asked Mark Bickford about this today, and one problem they ran into when trying to implement synthetic topology in Nuprl was that you seem to need some kind of parallel operator (like in PCF); now, Mark seemed to think that something like this was non-deterministic (and so he was not yet sure how to add it to Nuprl), but it should actually be deterministic, right?

p-or _|_ tt = tt
p-or tt _|_ = tt
p-or ff ff = ff

And everything else should just diverge. Or am I missing something?

ghost commented 9 years ago

I think whether it should be considered deterministic or not depends on how it is implemented and whether you consider that from the internal or external perspective. I don't know enough about what's possible yet with Howe's relation to see how it should work here but in the monadic approach it's pretty straightforward to implement:

https://github.com/freebroccolo/purescript-synthetic-semicomputable/blob/master/src/Synthetic/Topology/Time.purs#L42-L49