Total Denotational Semantics

Links
#21

One more follow up question: if we always only use takeD 10000 (or similar) to inspect the resulting terms, then why not just add that number as an argument to the denote function? What benefit does the guarded delay monad have over simple fuel-indexed functions?

I’m asking these questions now because I’m working on a definition of context-free languages which also require me to watch out for nontermination. I’m using a fuel-indexing approach now which seems to work fine, so I’d like to know of any potential future problems that I might face.

#22

You would also need to step-index Value then and would drown in step-indexing arithmetic. But otherwise, that’s viable. You could simplify the setup by not doing a denotational semantics at all, then you can’t have Fun and thus don’t need a step-indexed domain. The result is a definitional interpreter like this one.

Do note that denot already is the function that maps a Nat to “refinements”/“prefixes” of a T Value. You can see this if you look at the model of guarded dependent type theory, which is all about presheaves (to a first approximation: a countable family of sets S_i where S_{i+1} is included in S_i). I suggest you jump to Section 2 “The S topos” for a quick introduction. It’s not too hard to grasp and I couldn’t do it any better.
The point about guarded types however is that one does not want to reason in terms of this model because it’s tedious. See the C vs. assembler analogy in Total Denotational Semantics - #10 by sgraf.

1 Like