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

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.

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

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.

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.

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

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

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

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?

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.

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?

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…

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