2
$\begingroup$

I'm interested in proving correctness of the interpreter of Appel's compiler (appendix B), and compare it to the machine semantics given by Kennedy on his paper. The interpreter acts as a denotational semantics for the compiler's IR, effectively executing a syntactic object (as a datatype) and returning a computation on the host language. I have a formalization for the machine semantics already (available on GitHub), however, the algorithm is built relying on a type declared (in ML) as:

datatype dvalue = ... | FUNC of dvalue list -> answer | ...

The dvalue type (which is the result type of the interpreter) includes a negative recursive occurrence, which I understand is problematic. So my question is: is there any trick that could be used to formalize the algorithm such that I could still extract executable code from it?

I mean "trick" in the same sense that we can get general recursion by using a coinductive partiality monad, which I was already planning on using anyway since the algorithm does not necessarily terminate. I could, of course, model ML on top of Coq then the algorithm on top of it, but this would be an overkill for reasoning about the algorithm, specially as the extracted code wouldn't really match the original (so I'll leave that as a plan B). Unfortunately, changing this type would deviate too much from the algorithm I'd like to verify and prove correct.

Though I'm asking particularly about Coq (as I've already a bunch of stuff formalized in there...), if this can't be done, could Agda do something like that (perhaps with guarded types)?

$\endgroup$
4
  • 1
    $\begingroup$ You can axiomatize a domain (such as a dcpo) with some required properties, and when extracting instantiate it with the concrete OCaml (or whatever language you extract to) type. That is still probably overkill but less so.. $\endgroup$
    – Trebor
    Aug 9, 2023 at 3:05
  • 1
    $\begingroup$ Or perhaps just have a Axiom FuncType: Type that is implemented as dvalue list -> answer along with a retract that gets extracted to the identity function, which is significantly less overkill. $\endgroup$
    – cody
    Aug 14, 2023 at 21:39
  • $\begingroup$ @cody, I did think of that, but then I'd pose another question: assuming the introduction, elimination and some sort of computational rule seems enough to derive False. How could I write the algorithm, prove it correct with regard to the machine semantics, and make it in a convincing way, such that people would trust the proof? After all, I'd be assuming something that leads to an absurd in the mix. $\endgroup$ Aug 14, 2023 at 21:59
  • 3
    $\begingroup$ Are you sure you can inhabit False, even if you keep answer abstract? If abstract = unit then the assumption that we have a type D ≅ D list → answer is consistent (take D = unit). Therefore, if answer is kept abstract, you will not be able to inhabit False, or else you would be able to do it also when abstract = unit. $\endgroup$ Aug 15, 2023 at 7:18

2 Answers 2

3
$\begingroup$

Building on Cody's suggestion, the following might work for you. I will consider a simpler type that still captures the essence of the problem.

Define a structure which, given a type answer, produces a type T equivalent to list T -> answer.

Structure Fix (answer : Type) : Type := {
    carrier : Type ;
    f : carrier -> (list carrier -> answer) ;
    g : (list carrier -> answer) -> carrier ;
    fg_id : forall l x, f (g l) x = l x ;
    gf_id : forall y, g (f y) = y
}.

Now, crucially, make sure all the proofs that assume Fix answer do so for an abstract answer, i.e., a parameter can still be instantiated later. Any theorem so proved is consistent because Fix answer is consistent when answer = unit:

Lemma unit_eq : forall x y : unit, x = y.
Proof.
  intros [] []; reflexivity.
Qed.

Definition T : Fix unit.
Proof.
  refine {|
    carrier := unit ;
    f := fun _ _ => tt ;
    g := fun _ => tt
  |}.
  - intros l []; apply unit_eq.
  - apply unit_eq.
Qed.

To put it another way, if you can derive False from S : Fix answer, where answer is a parameter, then you can derive False straight up by instantiating answer := unit and S := T (defined above).

We might worry that in Coq we can prove that S : Fix answer implies answer ≅ unit, which would render the whole thing trivial. But this is not so, because there are semantic models of CIC in which Fix answer is inhabited for non-trivial answer. For example, I would imagine that something like Alex Simpson's Computational adequacy for recursive types in models of intuitionistic set theory would fit the bill.

You will not be able to use anything particular about answer by keeping it general. This should not cause trouble, as it is Appel's intention to keep answer abstract, anyhow.

$\endgroup$
1
  • $\begingroup$ Oh, you and @cody are right! I had noticed that I could derive an absurd from something like that when the answer is relevant, and indeed it's easy to check that Fix bool -> False (should I add the proof in here?), but I didn't think of the case where there's a single constructor (in the case of unit). As you say, if the answer type is kept polymorphic, this is fine, and this should probably be enough to prove correctness of the interpreter. Thank you both! $\endgroup$ Aug 16, 2023 at 19:18
0
$\begingroup$

If I understand you correctly you want to write an interpreter eval: CPS -> dvalue, but the original definition of dvalue was from a non-total programming language, where dvalue occurs in a non-strictl positive position like this, which is not valid in Coq:

data dvalue where
  Int    : int -> dvalue
  String : string -> dvalue
  Not    : (dvalue -> answer) -> dvalue  -- error: dvalue is not strictly positive
  ...

This reminds me of how one can write an interpreter with from an inductively specified language to an denotation specified recursively over its type. But another challenge is that your denotation is untyped. On the other hand the interpreter function should be (easily?) able to generate the type of the value, because every value constructor has a type.

Note that this doesn't mean that the input lanugage (seemingly called CPS) needs to be typed, it can stay untyped, only the dvalues generated by the interpreter should be labelled by the type they belong to.

I suppose the following could work. Define a types of the values:

data ty where
  int  : ty
  str  : ty
  func : ty -> ty
  ans  : ty

define a typed dvalue' recursively over the types

dvalue' : ty -> Type
dvalue' int      = integer
dvalue' str      = string
dvalue' (func s) = dvalue' s -> answer
dvalue' ans      = answer

define untyped dvalue as a typed dvalue' for some type

dvalue : Type
dvalue = Σ (t:ty), dvalue' t

Now eval can be defined as CPS -> dvalue.

The only addition to the untyped eval algorithm is that the types of the produced values need to be labelled by their type. So for example the evaluation of an integer primop, would produce a tuple of the value as specified originally, tagged additionally by an 'int' tag like (int, x+y). The evaluation of an record literal, would produce a tuple of the value as specified originally, tagged additionally by an 'int' tag like (int, x+y).

Now, functions are represented as functions in the denotation, and can be extracted to functions. I hope this helps somehow and I didn't miss any further details.


EDIT: The first version of this answer proposed using PHOAS, but that didn't match the question...

$\endgroup$
6
  • 2
    $\begingroup$ The way I read the question, it is not asking how to represent the abstract syntax of a programming language. It is asking how to implement an algorithm whose ML implementation uses a non-inductive recursive datatype. $\endgroup$ Aug 14, 2023 at 11:56
  • $\begingroup$ @AndrejBauer is right. I don't think using PHOAS can help me in here, because the algorithm needs both introduction and elimination for the dvalue type. Unfortunately I think that even just assuming those two is enough to derive False. $\endgroup$ Aug 14, 2023 at 19:27
  • $\begingroup$ Sorry, i seemed to have missed some details of the question. Anyway, I looked at Appendix B and it seems the dvalue type corresponds more to the target (denotation) of the interpreter and not the source (syntax). Here is another long-shot: Typically, when i write an interpreter the input is defined as an Inductive tm := ... but the output is defined recursively over their type (or when untyped, just a definition) (Definition dvalue := ... + (list dvalue -> answer) + ... ). Would that work for you? $\endgroup$
    – drcicero
    Aug 16, 2023 at 7:22
  • 1
    $\begingroup$ Ah, wait, that only works if it actually is a typed represented otherwise the recursion doesn't end either... $\endgroup$
    – drcicero
    Aug 16, 2023 at 7:32
  • $\begingroup$ I think i missed the point with PHOAS previously. I edited the answer with a new example on an idea that could help. $\endgroup$
    – drcicero
    Aug 16, 2023 at 9:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.