source: etc/campbell/dev-notes/2012-08-03-cost-loop-breaking.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: 952 bytes
Line 
1One of the key cost labelling properties is that a cost label appears in every
2loop (at the head, at the start).  In the structured traces existence proofs
3for RTLabs it takes the form of a proof that there are a finite number of local
4steps until the next cost label.  There are two problems with this:
5
61. This isn't a natural notion for the hypothesis, because it's a semantic
7   rather than a syntactic notion.  The obvious thing is to replace it with
8   a notion of instructions until cost label, which is fine except that you
9   can't leave the bound on the number of instructions implicit or you'll have
10   to write a nasty function to calculate one (by taking the maximum over all
11   paths).
12
132. There's also another notion for this that appeared later for the back-end,
14   defined as a predicate on top of structured traces.  We're going to need to
15   show that we can fulfill this, but first I should check that they're
16   actually using it.
Note: See TracBrowser for help on using the repository browser.