source: etc/campbell/dev-notes/2012-01-11-non-terminating-traces.txt

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 
1To build the non-terminating structural traces we need to do more than just
2write a function that mirrors the structure of the resulting data type.
3To know which (coinductive) constructor to use we must first examine the
4trace to find whether we encounter a label or a non-terminating function
5next (terminating function calls will be buried in the finite part of the
6trace).
7
8It should be possible to implement this process with a terminating function
9using the fact that the program is well-labelled (i.e., it isn't possible to
10spend an infinite amount of time in one function because you'll encounter a
11label).
12
13However, the current well-labelled predicate is given in purely syntactic
14terms: it requires the successors of branching instructions to be labels.
15This was sufficient for the finite traces because we already knew that they
16are terminating.  I will need to construct an additional criterion to catch
17loops and show that the traces enjoy it.
Note: See TracBrowser for help on using the repository browser.