source: etc/campbell/dev-notes/2013-02-05-form-of-traces.txt

Last change on this file was 3672, checked in by campbell, 3 years ago

I'd been keeping some notes in the repo; didn't commit these before

File size: 817 bytes
Line 
1The execution and exec_inf[_aux] definitions I wrote in common/SmallstepExec.ma
2are troublesome for several reasons:
3
4 1) The is_final check prevents unfolding, requiring that axiom until matita
5    provides some proper mechanism to do it;
6 2) branching ought to be handled when I/O is allowed;
7 3) split_trace is a bit of a pain when the final state is included;
8
9Alternatives:
10
11 a) An exec_n_steps function (like up_to_nth_step in common/Animation.ma, but
12    avoiding the coinductive stuff entirely), either taking a list of input
13    to satisfy I/O or returning the trace in the I/O monad.  We could also prove
14    this equivalent to the cofixpoint, so relating the full simulation result
15    and the intensional subtrace results.
16 b) Present an entirely static notion of trace
17
18... [abandoned here]
19
20
21not_wrong?
Note: See TracBrowser for help on using the repository browser.