module README where -- The code in this directory explores different ways to construct a -- coinductive big-step semantics which is indexed by some sort of -- possibly infinite traces. -- -- In every approach a semantics -- _HasTrace_ : Expr → Trace → Set -- is defined, associating a trace of messages to an expression. The -- intention is that e HasTrace ms should be inhabited iff e can emit -- exactly the messages in ms (in the order given by ms). -- I have investigated two languages Expr, one which is deterministic -- and one which is not. -- Deterministic language -- ────────────────────── -- The expressions come from a very simple language: import Deterministic.Expr -- First note that it is easy to construct (perhaps by mistake) an -- incorrect semantics which associates expressions not only with the -- intended trace but also with all traces which have the intended -- trace as a prefix: import Deterministic.Incorrect -- In an FP Lunch meeting I suggested the EasyToWorkWith approach as a -- workaround, but people thought that it was inelegant. I agree; a -- specification should be easy to understand. However, the -- EasyToWorkWith approach seems to be quite nice to work with, so it -- might be worth using this approach in proofs, after proving it -- equivalent to another approach. import Deterministic.EasyToWorkWith -- Thorsten Altenkirch suggested that I should define the semantics in -- terms of finite observations. The EasyToUnderstand approach talks -- about individual messages, and is easy to understand, but -- (sometimes) more awkward to work with. import Deterministic.EasyToUnderstand -- The LongestPrefix approach instead talks about finite prefixes of -- the trace. It may be somewhat harder to understand than -- EasyToUnderstand, though. import Deterministic.LongestPrefix -- Thorsten also suggested that one could use the Incorrect approach, -- but only accept the shortest possible trace. The resulting -- semantics appears to be less constructive than the others, though, -- and it also seems to be awkward to work with. import Deterministic.ShortestExtension -- The various approaches above, with the exception of Incorrect, are -- equivalent. Classical reasoning (encoded using double-negation) is -- used to show that ShortestExtension implies the others. import Deterministic.Equivalence -- The language is actually deterministic: import Deterministic.Deterministic -- Non-deterministic language -- ────────────────────────── -- Thorsten suggested that my approach might not generalise to -- non-deterministic languages, so I decided to investigate the issue. -- A non-deterministic language: import NonDeterministic.Expr -- The description of the incorrect semantics outlines in what way the -- language is non-deterministic: import NonDeterministic.Incorrect -- It turned out to be non-trivial to generalise some of the -- approaches to the non-deterministic setting. The easiest one was -- EasyToWorkWith. import NonDeterministic.EasyToWorkWith -- LongestPrefix was generalised partly based on Thorsten's -- suggestions. Thorsten wanted the semantics to be defined in terms -- of finite observations. Unfortunately the definition uses a -- coinductive definition which I am not very happy with. import NonDeterministic.LongestPrefix -- The two approaches are equivalent; this increases my confidence in -- their correctness. import NonDeterministic.Equivalence -- I refrained from generalising the other approaches, because it was -- far from obvious how to do so while keeping to the spirit of the -- definitions used for the deterministic language. -- One conclusion of the second phase of this experiment is that the -- EasyToWorkWith approach is quite flexible and easy to adapt to new -- situations. This can be important when experimenting with a new -- language.