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?

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.
```

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.

(BTW, for a _stack_ machine, you'd want `Add`

to have type `instr A`

not `instr A -> instr A -> instr A`

)

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)

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

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.

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.

I was sort of trying to have a 'program' as a `list instr`

and run through it while consuming input symbols till an accept instruction is reached.

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.

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?

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

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.

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: Jun 20 2024 at 11:02 UTC