Julin S (May 15 2023 at 17:08): Julin S (May 15 2023 at 17:08):Hi. I got a set of instructions to be used to run a VM function. Like this:
| i | instr |
|---+--------------+
| 0 | Const true; |
| 1 | Const false; |
| 2 | Goto 4; |
| 3 | Const true; |
| 4 | Goto 1 |
Where Goto k signifies a jump to instruction at index k.
I wrote this up as:
Inductive instr :=
| Const: bool -> instr
| Goto: nat -> instr.
Definition prog := list instr.
I wanted to get something like an epsilon-closure of an individual instruction. ie, the indices of non-Goto instructions that are reachable from a given instruction in a prog.
So I naïvely tried
Fixpoint eclosure_aux (p:prog) (i:nat) (visited:list nat): list nat :=
let inds := seq 0 (length p) in
let aug := list_prod inds p in
match List.nth i aug (0, Goto 0) with
| (i,x) =>
match x with
| Const _ => [i]
| Goto k =>
if List.existsb (fun a => Nat.eqb a k) visited then [i]
else i :: (eclosure_aux p k (i::visited))
end
end.
Definition eclosure (p:prog) (i:nat): list nat := eclosure_aux p i [].
(*
Cannot guess decreasing argument of fix.
*)
I was hoping to get something like:
Example p1 := [
Const true; (* 0 *)
Const false; (* 1 *)
Goto 4; (* 2 *)
Const true; (* 3 *)
Goto 1 (* 4 *)
].
Compute eclosure p1 2 [].
(* [2; 4; 1] *)
The function eclosure_aux can be made to terminate because of the visited argument which can be used to avoid infinite loops.
But how can we convince the type checker?
Is there a way?
Julin S (May 15 2023 at 17:12):Complete example:
Require Import List.
Import ListNotations.
Inductive instr :=
| Const: bool -> instr
| Goto: nat -> instr.
Definition prog := list instr.
Example p1 := [
Const true; (* 0 *)
Const false; (* 1 *)
Goto 4; (* 2 *)
Const true; (* 3 *)
Goto 1 (* 4 *)
].
Fail Fixpoint eclosure_aux (p:prog) (i:nat) (visited:list nat): list nat :=
let inds := seq 0 (length p) in
let aug := list_prod inds p in
match List.nth i aug (0, Goto 0) with
| (i,x) =>
match x with
| Const _ => [i]
| Goto k =>
if List.existsb (fun a => Nat.eqb a k) visited then [i]
else i :: (eclosure_aux p k (i::visited))
end
end.
Fail Definition eclosure (p:prog) (i:nat): list nat := eclosure_aux p i [].
We can't just add a fuel parameter, right? Since we can't tell in advance how long a goto-goto-goto-... chain would be (or could such info be baked into the type?)
Gaëtan Gilbert (May 15 2023 at 17:44):a chain is at most length p long so fuel should work AFAICT
Last updated: Oct 04 2023 at 19:01 UTC