source: etc/campbell/dev-notes/2012-03-30-flattening.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: 1015 bytes
Line 
1My plan was to show that the structured traces accurately represent the original
2flat traces by flattening them out.  However, while the structured traces are
3in Type[0], they actually contain very little real data because most of the
4information is made out of predicates in Prop:
5
6  record abstract_status : Type[1] ≝ {
7    as_status :> Type[0];
8    as_execute : as_status → as_status → Prop;
9    as_classifier : as_status → status_class → Prop;
10    as_costed : as_status → Prop;
11    as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
12  }.
13 
14The RTLabs version of as_execute includes the event trace (t),
15
16    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
17
18which we would need in order to reconstruct the flat trace, which would mean
19going from Prop to Type[0].  To get out of this mess we could:
20
21  1. Move as_execute into Type[0].
22  2. Only show a relation between the flat and structured traces.
23...
24
25Oh, wait.  It's executable.  I can just execute it.
Note: See TracBrowser for help on using the repository browser.