Encoding impure higher-order function with ktree

[alxest]

I am trying to shallow-embed an OCaml program with ktree. Its code is as follows:

let r: ((int -> int) ref) = ref (fun _ -> failwith "")

let myrec (g: (int -> int) -> (int -> int)): int -> int =
  r := (fun x -> g !r x); !r

let factorial: int -> int =
  let g f x =
    if x = 0 
    then 1
    else x * f (x - 1)
  in
  myrec g

let main = print_endline (string_of_int (factorial 5));

Although int -> int functions are pure in this minimized code, I would like decorate them with some effects (e.g., print) in my development. Therefore, I would like to encode int -> int as ktree E nat nat However, I am continuously facing universe inconsistency and failed to finish the formalization. Can someone help me finishing this?

Thanks a lot!

[Lysxia]

This is going to be tricky not only because of the higher-order nature of the problem, but also because it uses general recursion that's implicitly available through mutable (higher-order) references. A shallow embedding in Coq must make that recursion explicit, and because of that, compromises must be made regarding expressiveness.

That said, here's one possible translation by defunctionalizing the (int -> int) -> (int -> int) and int -> int functions used by the mutable reference (it's certainly going to take a lot more work to have a more modular solution):

https://gist.github.com/Lysxia/e9f8426d9543fcc03d92bd3fe1e88bda

[alxest]

Thanks a lot for your help, @Lysxia ! I read your code, and the compromises you have made look very appropriate. I guess I can do some more experiments on top of your implementation.

Meanwhile, I would like to understand the essence of the problem and brought some follow-up questions.

• What is the general recursion? I know this term in computational-theory context, but I don't think you intended this. (We can write Ackermann function in itree :D)
• A shallow embedding in Coq: If we do deep embedding, does the situation get better?
• Is the following understanding appropriate?: "The mrec combinator has type (ctx : D ~> itree (D +' E)) : D ~> itree E. When you see the type of ctx, it allows recursion, but it does not allow to modify the ctx itself. Hence, you cannot handle recursion with this combinator in the presence of self-modifying code (in C/Asm) or higher-order mutable state (in OCaml)"

Below is my past attempt to tackle this problem. https://gist.github.com/alxest/154f55aa021ca68fd4a366fb4e6d3844 I tried to encode in a way that is as close as possible with the original OCaml code, but the universe inconsistency was a show stopper. (I am not sure if this inconsistency is essential or not) The gist is self-contained and compiles with Coq 8.11.1 (exploiting the new flag, Unset Universe Checking.!)

[Lysxia]

What is the general recursion? I know this term in computational-theory context, but I don't think you intended this. (We can write Ackermann function in itree :D)

That is actually what I meant. More precisely, I was referring to the fact that your example provides a way to write arbitrary, unrestricted recursive functions (that may diverge), as opposed to well-founded or guarded recursive functions as found in Coq (that are guaranteed to terminate/be productive). Interaction trees do allow you to encode infinite loops somehow in Coq, but for that you must still use one of the recursion combinators (or cofix). In your example, there is actually no control-flow construct for recursion, that would otherwise be the natural place to use an itree recursion combinator. Without using one of those, it's impossible to define a diverging computation. But this example is very much about allowing general (i.e., unrestricted) recursion. That is an argument why there is no "naive" way of translating that program in Coq.

A shallow embedding in Coq: If we do deep embedding, does the situation get better?

"Deep embedding" is the intuitive approach of first defining the object language syntax as an inductive type, giving it some small step semantics (the language most likely has one, straightforward though tedious), and then iterating it (with fuel, as a relation, or as an itree, among other ways). I think of "deep embedding" as the way you can always follow when all else fails.

Is the following understanding appropriate?

That's the right idea overall, but the limitations about what we can express with this combinator are actually not as clear as that. If you think of D as program locations then indeed you have a problem with self-modifying code because the mapping ctx is fixed. But you can also think of D as actual fragments of code, which can be stored, modified, and executed. So we can accomodate for higher-order features to some extent.