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