非确定性的解释器（英文）

Suppose you have a toy specification with built-in nondeterminism, and you want to generate answers with respect to the specification:

type exp = EInt of int | EPair of exp * exp | ENdet of exp * exp
type ans = VInt of int | VPair of ans * ans

For example, from the following specification

EPair (ENdet (EInt 5) (EInt 6)) (ENdet (EInt 7) (EInt 8))

you might want to generate a bunch of possible answers:

VPair (VInt 5) (VInt 7)
VPair (VInt 5) (VInt 8)
VPair (VInt 6) (VInt 7)
VPair (VInt 6) (VInt 8)

The scene might be where you want to specify something with multiple sites of nondeterminism, ask the generator to come up with an answer, and successively give you other answers until you are satisfied.

The basic methodology is search. We want to construct a recursive procedure on the structure of a specification. For a sub-specification, it should know two sorts of computation:

• the computation that completes a whole answer and constructs a procedure for next whole answers, given the current sub-answer for the sub-specification and a procedure for next whole answers if the current sub-answer would leads to a subsequent unsatisfactoriness; and
• the computation to find next whole answers.

In this sense, the first computation has type $\mathsf{ans} \to \mathsf{next} \to \mathsf{ans} \times \mathsf{next}$, and the second one should be typed $\mathsf{next}$. A computation of type $\mathsf{next}$ is supposed to (i) either fail, or (ii) take no arguments, and when invoked it should return the next whole answer as well as a new $\mathsf{next}$ computation. Thus we have $\mathsf{next} \equiv \mathbf{1} + \mathbf{1} \to (\mathsf{ans} \times \mathsf{next})$. Therefore we use recursive types to model this mechanism.

type next = NFail | NCont of (unit -> ans * next)

Then it is straightforward to implement an interpreter:

let rec interp exp cont fail =
  match exp with
  | EInt n -> cont (VInt n) fail
  | EPair (e, e') -> interp e (fun v fail' -> interp e' (fun v' fail'' -> cont (VPair (v, v')) fail'') fail') fail
  | ENdet (e1, e2) -> interp e1 cont (NCont (fun () -> interp e2 cont fail))

The execution should be the following:

let (ans1, next1) = interp (EPair (ENdet (EInt 5) (EInt 6)) (ENdet (EInt 7) (EInt 8))) (fun v fail -> (v, fail)) NFail;;
(* val ans1 : ans = VPair (VInt 5, VInt 7) *)
(* val next1 : next = NCont <fun> *)
let (ans2, next2) = match next1 with NCont f -> f ();;
(* val ans2 : ans = VPair (VInt 5, VInt 8) *)
(* val next2 : next = NCont <fun> *)
let (ans3, next3) = match next2 with NCont f -> f ();;
(* val ans3 : ans = VPair (VInt 6, VInt 7) *)
(* val next3 : next = NCont <fun> *)
let (ans4, next4) = match next3 with NCont f -> f ();;
(* val ans4 : ans = VPair (VInt 6, VInt 8) *)
(* val next4 : next = NFail *)