Name | Last modified | Size | Description | |
---|---|---|---|---|

Parent Directory | - | |||

Agda.css | 13-Apr-2010 19:13 | 1.1K | ||

Data.Empty.html | 13-Apr-2010 19:13 | 3.8K | ||

Relation.Nullary.html | 13-Apr-2010 19:13 | 3.8K | ||

Data.Maybe.Core.html | 13-Apr-2010 19:13 | 4.6K | ||

Category.Monad.Ident..> | 13-Apr-2010 19:13 | 5.1K | ||

Algebra.RingSolver.S..> | 13-Apr-2010 19:13 | 5.2K | ||

Relation.Binary.Part..> | 13-Apr-2010 19:13 | 5.3K | ||

Category.Applicative..> | 13-Apr-2010 19:13 | 6.3K | ||

Algebra.FunctionProp..> | 13-Apr-2010 19:13 | 6.7K | ||

Category.Functor.html | 13-Apr-2010 19:13 | 7.0K | ||

Relation.Binary.EqRe..> | 13-Apr-2010 19:13 | 7.2K | ||

Relation.Nullary.Cor..> | 13-Apr-2010 19:13 | 7.9K | ||

Relation.Nullary.Pro..> | 13-Apr-2010 19:13 | 8.2K | ||

Coinduction.html | 13-Apr-2010 19:13 | 10K | ||

Level.html | 13-Apr-2010 19:13 | 10K | ||

Relation.Binary.Cons..> | 13-Apr-2010 19:13 | 11K | ||

Deterministic.Expr.html | 13-Apr-2010 19:13 | 12K | ||

Category.Monad.html | 13-Apr-2010 19:13 | 14K | ||

Relation.Binary.Simp..> | 13-Apr-2010 19:13 | 14K | ||

Deterministic.Incorr..> | 13-Apr-2010 19:13 | 14K | ||

README.html | 13-Apr-2010 19:13 | 14K | ||

NonDeterministic.Exp..> | 13-Apr-2010 19:13 | 15K | ||

NonDeterministic.Inc..> | 13-Apr-2010 19:13 | 16K | ||

Relation.Binary.Inde..> | 13-Apr-2010 19:13 | 17K | ||

Data.BoundedVec.Inef..> | 13-Apr-2010 19:13 | 18K | ||

Relation.Binary.Prop..> | 13-Apr-2010 19:13 | 18K | ||

Deterministic.Determ..> | 13-Apr-2010 19:13 | 19K | ||

Deterministic.EasyTo..> | 13-Apr-2010 19:13 | 20K | ||

Relation.Binary.Indu..> | 13-Apr-2010 19:13 | 21K | ||

Relation.Binary.Preo..> | 13-Apr-2010 19:13 | 21K | ||

Deterministic.Shorte..> | 13-Apr-2010 19:13 | 22K | ||

Data.Unit.html | 13-Apr-2010 19:13 | 22K | ||

NonDeterministic.Eas..> | 13-Apr-2010 19:13 | 23K | ||

Data.Conat.html | 13-Apr-2010 19:13 | 25K | ||

Data.Bool.html | 13-Apr-2010 19:13 | 26K | ||

Function.Injection.html | 13-Apr-2010 19:13 | 27K | ||

Data.Fin.Subset.html | 13-Apr-2010 19:13 | 27K | ||

Category.Applicative..> | 13-Apr-2010 19:13 | 28K | ||

Category.Monad.Index..> | 13-Apr-2010 19:13 | 32K | ||

Algebra.Operations.html | 13-Apr-2010 19:13 | 32K | ||

Algebra.Props.Abelia..> | 13-Apr-2010 19:13 | 34K | ||

Function.Bijection.html | 13-Apr-2010 19:13 | 36K | ||

Data.Sum.html | 13-Apr-2010 19:13 | 36K | ||

Function.Surjection...> | 13-Apr-2010 19:13 | 37K | ||

Deterministic.Longes..> | 13-Apr-2010 19:13 | 40K | ||

Deterministic.EasyTo..> | 13-Apr-2010 19:13 | 40K | ||

Relation.Binary.Inde..> | 13-Apr-2010 19:13 | 42K | ||

Algebra.Props.Ring.html | 13-Apr-2010 19:13 | 42K | ||

Relation.Nullary.Dec..> | 13-Apr-2010 19:13 | 43K | ||

Algebra.Morphism.html | 13-Apr-2010 19:13 | 45K | ||

Relation.Binary.Refl..> | 13-Apr-2010 19:13 | 47K | ||

NonDeterministic.Lon..> | 13-Apr-2010 19:13 | 48K | ||

Data.Fin.Subset.Prop..> | 13-Apr-2010 19:13 | 48K | ||

Function.LeftInverse..> | 13-Apr-2010 19:13 | 53K | ||

Function.html | 13-Apr-2010 19:13 | 53K | ||

Algebra.Props.Group...> | 13-Apr-2010 19:13 | 59K | ||

Algebra.FunctionProp..> | 13-Apr-2010 19:13 | 60K | ||

Algebra.RingSolver.A..> | 13-Apr-2010 19:13 | 61K | ||

Function.Equality.html | 13-Apr-2010 19:13 | 62K | ||

NonDeterministic.Equ..> | 13-Apr-2010 19:13 | 63K | ||

Relation.Unary.html | 13-Apr-2010 19:13 | 66K | ||

Function.Equivalence..> | 13-Apr-2010 19:13 | 67K | ||

Data.Maybe.html | 13-Apr-2010 19:13 | 75K | ||

Relation.Binary.Prop..> | 13-Apr-2010 19:13 | 82K | ||

Relation.Binary.Cons..> | 13-Apr-2010 19:13 | 88K | ||

Data.Product.html | 13-Apr-2010 19:13 | 91K | ||

Data.Vec.N-ary.html | 13-Apr-2010 19:13 | 99K | ||

Data.Fin.html | 13-Apr-2010 19:13 | 103K | ||

Relation.Nullary.Uni..> | 13-Apr-2010 19:13 | 104K | ||

Data.Fin.Props.html | 13-Apr-2010 19:13 | 120K | ||

Relation.Nullary.Neg..> | 13-Apr-2010 19:13 | 123K | ||

Data.List.NonEmpty.html | 13-Apr-2010 19:13 | 123K | ||

Data.Nat.html | 13-Apr-2010 19:13 | 124K | ||

Data.Fin.Dec.html | 13-Apr-2010 19:13 | 129K | ||

Relation.Binary.Core..> | 13-Apr-2010 19:13 | 132K | ||

Relation.Binary.html | 13-Apr-2010 19:13 | 140K | ||

Algebra.RingSolver.L..> | 13-Apr-2010 19:13 | 145K | ||

Function.Inverse.html | 13-Apr-2010 19:13 | 152K | ||

Algebra.html | 13-Apr-2010 19:13 | 155K | ||

Data.Colist.html | 13-Apr-2010 19:13 | 161K | ||

Data.Vec.html | 13-Apr-2010 19:13 | 181K | ||

Algebra.RingSolver.html | 13-Apr-2010 19:13 | 196K | ||

Algebra.Structures.html | 13-Apr-2010 19:13 | 211K | ||

Data.List.html | 13-Apr-2010 19:13 | 215K | ||

Relation.Binary.Prod..> | 13-Apr-2010 19:13 | 224K | ||

Deterministic.Equiva..> | 13-Apr-2010 19:13 | 264K | ||

Relation.Binary.Sum...> | 13-Apr-2010 19:13 | 331K | ||

Data.Nat.Properties...> | 13-Apr-2010 19:13 | 399K | ||

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.