Stream: Coq users

Topic: Denotational semantics without excluded middle

Christopher Lam (May 11 2023 at 19:32):

Is it possible to define a denotational semantics for an imperative language like imp without using excluded middle/more admitted axioms? https://xavierleroy.org/courses/Marktoberdorf-2009/notes.pdf defines the denotational semantics using both excluded middle and an axiom of description, and I don't see a good way of getting around this

Guillaume Melquiond (May 12 2023 at 05:12):

Presumably, you only need those axioms if you want to deal with infinite executions. And even so, I would expect that some much weaker axioms (e.g., limited principle of omniscience) could be used instead.

Karl Palmskog (May 12 2023 at 06:35):

for constructive approach to infinite semantics in Coq, see Uustalu and Nakata series of papers, https://arxiv.org/pdf/1412.6579.pdf - but only trace-based I guess

Frédéric Besson (May 12 2023 at 08:56):

If [[c]] : state -> (state -> Prop), you can probably define a "denotational" semantics by recursion over c computing a least fixpoint for the while.
And proving that [[c]] s is always a singleton.

Meven Lennon-Bertrand (May 12 2023 at 09:17):

To precise Frédéric's answer: excluded middle/description are necessary to present $\llbracket \cdot \rrbracket$ as a function $\llbracket c \rrbracket : \texttt{state} \to \texttt{result}$. However you can instead define $\llbracket c \rrbracket$ as a (partial) functional relation, ie $\llbracket c \rrbracket : \texttt{state} \to \texttt{state} \to \texttt{Prop}$, such that for each $s$ there is at most one $s'$ such that $\llbracket c \rrbracket~s~s'$. The relation is easy to define: simply interpret the clauses in section 2.6 as defining an inductive proposition.

Now excluded middle + description are exactly what lets one in general turn such a partial functional relation into a function (and this has nothing to do with denotational semantics). Functions are in general slightly easier to work with, first because in a type theory like Coq's, you get help from computation (although, if your function was defined using axioms such as description, you will not have this), and second because you can directly write $P~(f~y)$, rather than having to say "if $R~x~y$ then $P~y$". But up to these small differences, you can get away with functional relations very well, and handle your denotational semantics nicely.

Frédéric Besson (May 12 2023 at 10:10):

I propose a variant : not an inductive definition but a recursive function over c (not of type state -> result) but (state -> (state -> Prop)).

Meven Lennon-Bertrand (May 12 2023 at 12:36):

This won't work: because of while, you cannot define this as a terminating function. However, once you have defined the inductive relation, you can define a recursive function that does one depth of unfolding, see here for an example

Kenji Maillard (May 12 2023 at 15:57):

You could use the impredicative nature of Prop to define a function using arbitrary fixpoints though.

Christopher Lam (May 12 2023 at 18:01):

To back up to why I want this, I want to basically be able to say "for each program p and state s, running p on s either terminates or runs forever". I am fairly certain that this is going to require admitting another axiom, which I would prefer not to do. The denotational semantics that I linked would let me do this I think because they would let me destruct over the codomain of the denotation function. Is there another way of doing this that I'm missing that doesn't need an admitted axiom?

Paolo Giarrusso (May 12 2023 at 20:12):

That sounds very close to deciding termination, but maybe using not (not (terminates \/ loops)) would let you encode excluded middle without technically assuming it, if you think it's a worthwhile.

Paolo Giarrusso (May 12 2023 at 20:17):

Technically, using terminates \/ loops doesn't let you extract a decider (because Prop is erased), but I'd expect an an axiom-free proof must still prove the disjunction constructively (existence property) which isn't possible. However, I point this out because I'm not confident enough and I expect corrections here... Is it possible to prove the existence property for Coq's Prop via some "proof-relevant" model? It sounds like it'd have to be anticlassical... Would collapsing Prop with impredicative Set fail, and where?

Meven Lennon-Bertrand (May 15 2023 at 09:05):

Indeed, I'd say that "for each program p and state s, running p on s either terminates or runs forever" is a form of excluded middle (more specifically, of the limited principle of omniscience), and I don't expect it to be provable without axiom (although proving this formally would indeed mean showing some witness property for Prop-valued disjunction, which is no small feat). However, all usual standard techniques to deal with classical logic in a constructive meta-theory apply here, including double-negation translation, admitting an axiom…

Steve Zdancewic (May 17 2023 at 22:49):

If you are ok with working in a nontermination monad, you can maybe take a different route by using the techniques in, e.g., the interaction trees library, which uses coinductive datatypes to avoid using axioms when defining the semantics. See https://github.com/DeepSpec/InteractionTrees and the example hoare_example/Imp.v. You will still need excluded middle if you want to case-analyze on program termination, but it is sometimes possible to give more constructive statements of properties by embracing coinduction.

Last updated: Oct 04 2023 at 23:01 UTC