Stream: Coq users

Topic: Jump instr and infinite loop

Julin S (Mar 12 2023 at 06:11):

I got a set of instructions like Jump, Add, etc.

I was trying to make a stack machine to evaluate a list of these instructions (as in a program).

machine: list (instr A) -> list A -> bool

The machine starts from the first instruction and unless current instruction is a Jump, consumes one input symbol and moves on to the next instruction.

If it's a Jump instruction, no input symbol is consumed and the control merely moves to the location in program named by the Jump.

But the problem is that we could have a scenario like this:

| Location | Instruction |
|----------+-------------|
|        0 | Jump 1      |
|        1 | Jump 0      |

which is an infinite loop and the machine function won't terminate.

Is there a way to rule out such possibilities?

Maybe at the type level?

Julin S (Mar 12 2023 at 06:13):

My instr type is somewhat like:

Inductive instr (A:Type) : Type :=
| Const: nat -> instr A
| Add: instr A -> instr A -> instr A
| Jump: nat -> instr A.

Stefan Haan (Mar 12 2023 at 06:24):

You could add a fuel parameter to your evaluation function, so it executes a fixed number of steps at maximum. That some programs do not terminate is just nature of computation, at least if your computing concept wants to be Turing complete. You can also have a look at https://github.com/uds-psl/coq-library-undecidability which defines some machines like this.

Paolo Giarrusso (Mar 12 2023 at 08:52):

(BTW, for a _stack_ machine, you'd want Add to have type instr A not instr A -> instr A -> instr A)

Paolo Giarrusso (Mar 12 2023 at 08:57):

there are languages where a type system can _easily_ forbid non-terminating programs*, but AFAIK stack machines with a Jump instructions aren't one of those

• (together with some terminating programs! termination isn't decidable, while type systems are typically decidable)

Karl Palmskog (Mar 12 2023 at 11:24):

alternative approach: define executions as coinductive possibly-infinite lists, then reason assuming a finiteness predicate on an execution

Dominique Larchey-Wendling (Mar 12 2023 at 18:32):

In the Coq library of Undecidability proofs, you may want to look at Minsky machines or binary stack machines. The computation is described as a relation because it might not terminate, typically on self loops or cycles like the two jumps above. Hence total functions cannot represent such relations unless guarded by a termination certificate.

Julin S (Mar 13 2023 at 03:33):

Paolo Giarrusso said:

(BTW, for a _stack_ machine, you'd want Add to have type instr A not instr A -> instr A -> instr A)

My bad.. It's not a stack machine. That was a mistake.

Julin S (Mar 13 2023 at 03:34):

I was sort of trying to have a 'program' as a list instrand run through it while consuming input symbols till an accept instruction is reached.

Julin S (Mar 13 2023 at 03:36):

But having a jump instruction pointing to another jump instruction would cause infinite loop without consuming input symbols.
Ideally, I was looking for a way to prohibit a jump from pointing to another jump.

Julin S (Mar 13 2023 at 03:45):

Karl Palmskog said:

alternative approach: define executions as coinductive possibly-infinite lists, then reason assuming a finiteness predicate on an execution

Finiteness predicate as in a proof that the execution would always terminate? How can we have that?

Pierre Castéran (Mar 13 2023 at 06:32):

I don't know if it may help, but this chapter presents examples about finite or infinite streams:
https://www-sop.inria.fr/members/Yves.Bertot/coqart-chapter13.pdf
Exercices and examples for recent versions of Coq are maintained by Coq community
https://github.com/coq-community/coq-art/tree/master/ch13_co_inductive_types

Karl Palmskog (Mar 13 2023 at 06:52):

Julin S said:

Finiteness predicate as in a proof that the execution would always terminate? How can we have that?

let's say you only want to prove something about when a program/process terminates (even when the setting is such that divergence is possible). Then, you can restrict yourself to the programs that actually terminate by adding a finite execution assumption. At some level, it's equivalent to describing computations using relations.

Paolo Giarrusso (Mar 13 2023 at 07:30):

prohibit a jump from pointing to another jump

You can enforce such things with well-forcedness predicates, but that alone won't forbid loops; you'd also need to restrict backward jumps or forbid them completely.

Last updated: Oct 04 2023 at 19:01 UTC