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.