![[ICO]](/icons/blank.gif){kind=icon}
![[PARENTDIR]](/icons/back.gif){kind=icon}
![[TXT]](/icons/text.gif){kind=icon}
------------------------------------------------------------------------ -- Code related to the paper Mixing Induction and Coinduction -- -- Nils Anders Danielsson ------------------------------------------------------------------------ module README where ------------------------------------------------------------------------ -- Section 3: An ad-hoc method for making corecursive definitions -- guarded -- A definition of the stream of Fibonacci numbers, as well -- as a definition of the Hamming numbers. import StreamProg -- Proofs of the map-iterate property and iterate fusion. import MapIterate -- A somewhat more elaborate/complicated variant of the method which -- can handle functions like tail. import SingletonChunks -- A generalised variant of (parts of) SingletonChunks, plus some -- extra examples. import ArbitraryChunks -- Implementations of the Thue-Morse sequence, using non-uniform chunk -- sizes. import ThueMorse import ThueMorseLeq -- Another variant which can handle tail. I believe that this one has -- limited applicability. import LargeCombinators -- An example which shows that nested applications of the defined -- function can be handled. import Nested -- A formalisation of parts of Ralf Hinze's paper "Streams and Unique -- Fixed Points". import Stream import Stream.Programs import Stream.Equality import Stream.Pointwise import Hinze.Lemmas import Hinze.Section2-4 import Hinze.Section3 import Hinze.Simplified.Section2-4 import Hinze.Simplified.Section3 -- By indexing the program and WHNF types on a universe one can handle -- several types at the same time. import UniverseIndex -- Breadth-first labelling of trees, /almost/ implementing the classic -- tie-the-recursive-knot algorithm due to Jeremy Gibbons and Geraint -- Jones (see "Linear-time Breadth-first Tree Algorithms: An Exercise -- in the Arithmetic of Folds and Zips", or Chris Okasaki's -- explanation in "Breadth-First Numbering: Lessons from a Small -- Exercise in Algorithm Design"). Proper sharing is not maintained, -- though, so this implementation is far from being linear in the size -- of the tree. import Stream import Tree import BreadthFirst.Universe import BreadthFirst.Programs import BreadthFirst -- A simplified variant of the code above, without any correctness -- statement or proof. import BreadthFirstWithoutProof -- A solution to a problem posed by Venanzio Capretta: The equation -- -- φ s = s ⋎ φ (evens (φ s)) -- -- has at most one solution. (Notice the nested uses of φ, and the use -- of evens which removes every other element from its input.) import VenanziosProblem -- A sound, inductive approximation of stream equality. import InductiveStreamEquality ------------------------------------------------------------------------ -- Section 4: Subtyping for recursive types -- Formalisation of subtyping for recursive types, partly based on -- "Coinductive Axiomatization of Recursive Type Equality and -- Subtyping" by Michael Brandt and Fritz Henglein. import RecursiveTypes -- One must exercise caution when using the technique advertised in -- Section 4. The following module shows that, in a coinductive -- setting, it is not always sound to postulate admissible rules -- (inductively). import AdmissibleButNotPostulable ------------------------------------------------------------------------ -- Section 5: Total parser combinators -- The following code may not match the paper exactly. See the paper -- Total Parser Combinators for more information. import TotalParserCombinators ------------------------------------------------------------------------ -- Section 6: Big-step semantics for both converging and diverging -- computations -- A definition of a big-step semantics which handles termination and -- non-termination at the same time, without duplication of rules. -- Partly based on Leroy and Grall's "Coinductive big-step operational -- semantics" and Cousot and Cousot's "Bi-inductive structural -- semantics". import Lambda -- An example showing how the list and colist types can be "unified". import DataAndCodata ------------------------------------------------------------------------ -- Section 7: Related work -- An investigation of nested fixpoints of the form μX.νY.… in Agda. -- It turns out that they cannot be represented directly. import MuNu -- An implementation of "A Unifying Approach to Recursive and -- Co-recursive Definitions" by Pietro Di Gianantonio and Marino -- Miculan. Contains one postulate. import Contractive import Contractive.Function import Contractive.Stream import Contractive.Examples ------------------------------------------------------------------------ -- Code which is not directly related to any particular section in the -- paper -- Various definitions of "true infinitely often", along with -- comparisons of the definitions. import InfinitelyOften