Index of /~nad/listings/traces

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Agda.css 13-Apr-2010 19:13 1.1K 
[TXT]Data.Empty.html 13-Apr-2010 19:13 3.8K 
[TXT]Relation.Nullary.html 13-Apr-2010 19:13 3.8K 
[TXT]Data.Maybe.Core.html 13-Apr-2010 19:13 4.6K 
[TXT]Category.Monad.Ident..>13-Apr-2010 19:13 5.1K 
[TXT]Algebra.RingSolver.S..>13-Apr-2010 19:13 5.2K 
[TXT]Relation.Binary.Part..>13-Apr-2010 19:13 5.3K 
[TXT]Category.Applicative..>13-Apr-2010 19:13 6.3K 
[TXT]Algebra.FunctionProp..>13-Apr-2010 19:13 6.7K 
[TXT]Category.Functor.html 13-Apr-2010 19:13 7.0K 
[TXT]Relation.Binary.EqRe..>13-Apr-2010 19:13 7.2K 
[TXT]Relation.Nullary.Cor..>13-Apr-2010 19:13 7.9K 
[TXT]Relation.Nullary.Pro..>13-Apr-2010 19:13 8.2K 
[TXT]Coinduction.html 13-Apr-2010 19:13 10K 
[TXT]Level.html 13-Apr-2010 19:13 10K 
[TXT]Relation.Binary.Cons..>13-Apr-2010 19:13 11K 
[TXT]Deterministic.Expr.html13-Apr-2010 19:13 12K 
[TXT]Category.Monad.html 13-Apr-2010 19:13 14K 
[TXT]Relation.Binary.Simp..>13-Apr-2010 19:13 14K 
[TXT]Deterministic.Incorr..>13-Apr-2010 19:13 14K 
[TXT]README.html 13-Apr-2010 19:13 14K 
[TXT]NonDeterministic.Exp..>13-Apr-2010 19:13 15K 
[TXT]NonDeterministic.Inc..>13-Apr-2010 19:13 16K 
[TXT]Relation.Binary.Inde..>13-Apr-2010 19:13 17K 
[TXT]Data.BoundedVec.Inef..>13-Apr-2010 19:13 18K 
[TXT]Relation.Binary.Prop..>13-Apr-2010 19:13 18K 
[TXT]Deterministic.Determ..>13-Apr-2010 19:13 19K 
[TXT]Deterministic.EasyTo..>13-Apr-2010 19:13 20K 
[TXT]Relation.Binary.Indu..>13-Apr-2010 19:13 21K 
[TXT]Relation.Binary.Preo..>13-Apr-2010 19:13 21K 
[TXT]Deterministic.Shorte..>13-Apr-2010 19:13 22K 
[TXT]Data.Unit.html 13-Apr-2010 19:13 22K 
[TXT]NonDeterministic.Eas..>13-Apr-2010 19:13 23K 
[TXT]Data.Conat.html 13-Apr-2010 19:13 25K 
[TXT]Data.Bool.html 13-Apr-2010 19:13 26K 
[TXT]Function.Injection.html13-Apr-2010 19:13 27K 
[TXT]Data.Fin.Subset.html 13-Apr-2010 19:13 27K 
[TXT]Category.Applicative..>13-Apr-2010 19:13 28K 
[TXT]Category.Monad.Index..>13-Apr-2010 19:13 32K 
[TXT]Algebra.Operations.html13-Apr-2010 19:13 32K 
[TXT]Algebra.Props.Abelia..>13-Apr-2010 19:13 34K 
[TXT]Function.Bijection.html13-Apr-2010 19:13 36K 
[TXT]Data.Sum.html 13-Apr-2010 19:13 36K 
[TXT]Function.Surjection...>13-Apr-2010 19:13 37K 
[TXT]Deterministic.Longes..>13-Apr-2010 19:13 40K 
[TXT]Deterministic.EasyTo..>13-Apr-2010 19:13 40K 
[TXT]Relation.Binary.Inde..>13-Apr-2010 19:13 42K 
[TXT]Algebra.Props.Ring.html13-Apr-2010 19:13 42K 
[TXT]Relation.Nullary.Dec..>13-Apr-2010 19:13 43K 
[TXT]Algebra.Morphism.html 13-Apr-2010 19:13 45K 
[TXT]Relation.Binary.Refl..>13-Apr-2010 19:13 47K 
[TXT]NonDeterministic.Lon..>13-Apr-2010 19:13 48K 
[TXT]Data.Fin.Subset.Prop..>13-Apr-2010 19:13 48K 
[TXT]Function.LeftInverse..>13-Apr-2010 19:13 53K 
[TXT]Function.html 13-Apr-2010 19:13 53K 
[TXT]Algebra.Props.Group...>13-Apr-2010 19:13 59K 
[TXT]Algebra.FunctionProp..>13-Apr-2010 19:13 60K 
[TXT]Algebra.RingSolver.A..>13-Apr-2010 19:13 61K 
[TXT]Function.Equality.html 13-Apr-2010 19:13 62K 
[TXT]NonDeterministic.Equ..>13-Apr-2010 19:13 63K 
[TXT]Relation.Unary.html 13-Apr-2010 19:13 66K 
[TXT]Function.Equivalence..>13-Apr-2010 19:13 67K 
[TXT]Data.Maybe.html 13-Apr-2010 19:13 75K 
[TXT]Relation.Binary.Prop..>13-Apr-2010 19:13 82K 
[TXT]Relation.Binary.Cons..>13-Apr-2010 19:13 88K 
[TXT]Data.Product.html 13-Apr-2010 19:13 91K 
[TXT]Data.Vec.N-ary.html 13-Apr-2010 19:13 99K 
[TXT]Data.Fin.html 13-Apr-2010 19:13 103K 
[TXT]Relation.Nullary.Uni..>13-Apr-2010 19:13 104K 
[TXT]Data.Fin.Props.html 13-Apr-2010 19:13 120K 
[TXT]Relation.Nullary.Neg..>13-Apr-2010 19:13 123K 
[TXT]Data.List.NonEmpty.html13-Apr-2010 19:13 123K 
[TXT]Data.Nat.html 13-Apr-2010 19:13 124K 
[TXT]Data.Fin.Dec.html 13-Apr-2010 19:13 129K 
[TXT]Relation.Binary.Core..>13-Apr-2010 19:13 132K 
[TXT]Relation.Binary.html 13-Apr-2010 19:13 140K 
[TXT]Algebra.RingSolver.L..>13-Apr-2010 19:13 145K 
[TXT]Function.Inverse.html 13-Apr-2010 19:13 152K 
[TXT]Algebra.html 13-Apr-2010 19:13 155K 
[TXT]Data.Colist.html 13-Apr-2010 19:13 161K 
[TXT]Data.Vec.html 13-Apr-2010 19:13 181K 
[TXT]Algebra.RingSolver.html13-Apr-2010 19:13 196K 
[TXT]Algebra.Structures.html13-Apr-2010 19:13 211K 
[TXT]Data.List.html 13-Apr-2010 19:13 215K 
[TXT]Relation.Binary.Prod..>13-Apr-2010 19:13 224K 
[TXT]Deterministic.Equiva..>13-Apr-2010 19:13 264K 
[TXT]Relation.Binary.Sum...>13-Apr-2010 19:13 331K 
[TXT]Data.Nat.Properties...>13-Apr-2010 19:13 399K 

README
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.