|
Last change
on this file was
2394,
checked in by campbell, 7 years ago
|
|
I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.
|
|
File size:
956 bytes
|
| Line | |
|---|
| 1 | To build the non-terminating structural traces we need to do more than just |
|---|
| 2 | write a function that mirrors the structure of the resulting data type. |
|---|
| 3 | To know which (coinductive) constructor to use we must first examine the |
|---|
| 4 | trace to find whether we encounter a label or a non-terminating function |
|---|
| 5 | next (terminating function calls will be buried in the finite part of the |
|---|
| 6 | trace). |
|---|
| 7 | |
|---|
| 8 | It should be possible to implement this process with a terminating function |
|---|
| 9 | using the fact that the program is well-labelled (i.e., it isn't possible to |
|---|
| 10 | spend an infinite amount of time in one function because you'll encounter a |
|---|
| 11 | label). |
|---|
| 12 | |
|---|
| 13 | However, the current well-labelled predicate is given in purely syntactic |
|---|
| 14 | terms: it requires the successors of branching instructions to be labels. |
|---|
| 15 | This was sufficient for the finite traces because we already knew that they |
|---|
| 16 | are terminating. I will need to construct an additional criterion to catch |
|---|
| 17 | loops and show that the traces enjoy it. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
