M-types #
M types are potentially infinite tree-like structures. They are defined as the greatest fixpoint of a polynomial functor.
- continue: {F : PFunctor} → PFunctor.Approx.CofixA F 0
- intro: {F : PFunctor} → {n : ℕ} → (a : F.A) → (PFunctor.B F a → PFunctor.Approx.CofixA F n) → PFunctor.Approx.CofixA F (Nat.succ n)
CofixA F n
is an n
level approximation of an M-type
Instances For
default inhabitant of CofixA
Equations
- PFunctor.Approx.CofixA.default F 0 = PFunctor.Approx.CofixA.continue
- PFunctor.Approx.CofixA.default F (Nat.succ n) = PFunctor.Approx.CofixA.intro default fun x => PFunctor.Approx.CofixA.default F n
Instances For
The label of the root of the tree for a non-trivial approximation of the cofix of a pfunctor.
Instances For
for a non-trivial approximation, return all the subtrees of the root
Instances For
- continu: ∀ {F : PFunctor} (x : PFunctor.Approx.CofixA F 0) (y : PFunctor.Approx.CofixA F 1), PFunctor.Approx.Agree x y
- intro: ∀ {F : PFunctor} {n : ℕ} {a : F.A} (x : PFunctor.B F a → PFunctor.Approx.CofixA F n) (x' : PFunctor.B F a → PFunctor.Approx.CofixA F (n + 1)), (∀ (i : PFunctor.B F a), PFunctor.Approx.Agree (x i) (x' i)) → PFunctor.Approx.Agree (PFunctor.Approx.CofixA.intro a x) (PFunctor.Approx.CofixA.intro a x')
Relation between two approximations of the cofix of a pfunctor that state they both contain the same data until one of them is truncated
Instances For
truncate a
turns a
into a more limited approximation
Equations
- PFunctor.Approx.truncate (PFunctor.Approx.CofixA.intro a a_1) = PFunctor.Approx.CofixA.continue
- PFunctor.Approx.truncate (PFunctor.Approx.CofixA.intro i f) = PFunctor.Approx.CofixA.intro i (PFunctor.Approx.truncate ∘ f)
Instances For
sCorec f i n
creates an approximation of height n
of the final coalgebra of f
Equations
- PFunctor.Approx.sCorec f x 0 = PFunctor.Approx.CofixA.continue
- PFunctor.Approx.sCorec f x (Nat.succ n) = PFunctor.Approx.CofixA.intro (f x).fst fun i => PFunctor.Approx.sCorec f (Sigma.snd F.A (fun x => PFunctor.B F x → X) (f x) i) n
Instances For
Path F
provides indices to access internal nodes in Corec F
Instances For
- approx : (n : ℕ) → PFunctor.Approx.CofixA F n
An
n
-th level approximation, for each depthn
- consistent : PFunctor.Approx.AllAgree s.approx
Each approximation agrees with the next
Internal definition for M
. It is needed to avoid name clashes
between M.mk
and M.cases_on
and the declarations generated for
the structure
Instances For
For polynomial functor F
, M F
is its final coalgebra
Instances For
Corecursor for the M-type defined by F
.
Instances For
given a tree generated by F
, head
gives us the first piece of data
it contains
Instances For
return all the subtrees of the root of a tree x : M F
Instances For
select a subtree using an i : F.Idx
or return an arbitrary tree if
i
designates no subtree of x
Instances For
unfold an M-type
Instances For
generates the approximations needed for M.mk
Instances For
constructor for M-types
Instances For
- trivial: ∀ {F : PFunctor} (x y : PFunctor.M F), PFunctor.M.Agree' 0 x y
- step: ∀ {F : PFunctor} {n : ℕ} {a : F.A} (x y : PFunctor.B F a → PFunctor.M F) {x' y' : PFunctor.M F}, x' = PFunctor.M.mk { fst := a, snd := x } → y' = PFunctor.M.mk { fst := a, snd := y } → (∀ (i : PFunctor.B F a), PFunctor.M.Agree' n (x i) (y i)) → PFunctor.M.Agree' (Nat.succ n) x' y'
Agree' n
relates two trees of type M F
that
are the same up to depth n
Instances For
destructor for M-types
Instances For
destructor for M-types
Instances For
destructor for M-types, similar to casesOn
but also
gives access directly to the root and subtrees on an M-type
Instances For
- nil: ∀ {F : PFunctor} (x : PFunctor.M F), PFunctor.M.IsPath [] x
- cons: ∀ {F : PFunctor} (xs : PFunctor.Approx.Path F) {a : F.A} (x : PFunctor.M F) (f : PFunctor.B F a → PFunctor.M F) (i : PFunctor.B F a), x = PFunctor.M.mk { fst := a, snd := f } → PFunctor.M.IsPath xs (f i) → PFunctor.M.IsPath ({ fst := a, snd := i } :: xs) x
IsPath p x
tells us if p
is a valid path through x
Instances For
follow a path through a value of M F
and return the subtree
found at the end of the path if it is a valid path for that value and
return a default tree
Equations
- One or more equations did not get rendered due to their size.
- PFunctor.M.isubtree [] x = x
Instances For
similar to isubtree
but returns the data at the end of the path instead
of the whole subtree
Instances For
- head : ∀ {a a' : F.A} {f : PFunctor.B F a → PFunctor.M F} {f' : PFunctor.B F a' → PFunctor.M F}, R (PFunctor.M.mk { fst := a, snd := f }) (PFunctor.M.mk { fst := a', snd := f' }) → a = a'
The head of the trees are equal
- tail : ∀ {a : F.A} {f f' : PFunctor.B F a → PFunctor.M F}, R (PFunctor.M.mk { fst := a, snd := f }) (PFunctor.M.mk { fst := a, snd := f' }) → ∀ (i : PFunctor.B F a), R (f i) (f' i)
The tails are equal
Bisimulation is the standard proof technique for equality between infinite tree-like structures
Instances For
corecursor for M F
with swapped arguments
Instances For
corecursor where the state of the computation can be sent downstream in the form of a recursive call
Instances For
corecursor where it is possible to return a fully formed value at any point of the computation