source: etc/campbell/dev-notes/2012-01-06-tracetermination.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: 999 bytes
Line 
1I have three mutually recursive functions for building the structured traces
2from flat RTLabs traces for a terminating function.  The guardedness check for
3these fails for two reasons:
4
5  1. some of the uses of the other functions pass the "decreasing" argument
6     (the termination proof) without making it smaller, because the "real"
7     processing happens in another function; and
8
9  2. recursive calls consume a prefix of the termination proof and the
10     remainder is returned for building more of the structured trace, but
11     matita doesn't know that this is smaller than the original argument.
12
13Both of these could be solved at the same time if I produce a termination
14counter together with a proof that it is at least as large as 3 times the
15length of the termination proof.
16
17For now I've put the termination definition into Type[0] rather than Prop
18so that I can define the length function.  This might cause trouble when
19applying the excluded middle, but I'll worry about that later.
Note: See TracBrowser for help on using the repository browser.