source: etc/campbell/dev-notes/2012-02-17-nontermination.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: 1.4 KB
Line 
1When producing the non-terminating RTLabs structured traces we need to know
2that non-termination is preserved after adding a terminating call; that is
3(using the contrapositive) given a proof of
4
51.  will_return ge d state_after trace_after
6
7and from the termination oracle
8
92.  will_return ge O call_state call_trace
10
11we should be able to show
12
13  will_return ge (S d) call_state call_trace
14
15so as to demonstrate that terminating after the call implies that we know that
16we will terminate before the call.  The problem is that we have no connection
17between the state and trace after the call, and their counterparts before the
18call.
19
20I foolishly tried showing and using the fact that trace_after contains
21call_trace, but this isn't strong enough because that doesn't show that
22call_trace immediately follows the call (it could be inside or after it, too).
23
24Essentially we need to add some property to make_label_return.  One possibility
25is to write a function to extract the state and trace from the end of 2 and
26show that it's also the end of the structured trace.  Another would be to make
27the end state and trace parameters of will_return, but that makes
28make_label_return a bit horrible (and would make it harder for the termination
29proof to be moved to Prop later, if desired).  We could also maintain a CPS-like
30property (give me more termination proof and I'll give you one from the start).
31
Note: See TracBrowser for help on using the repository browser.