From c4b021dfd3e462a77cb37ba349528cf4b0fe8ce1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?William=20S=C3=B8rensen?= Date: Fri, 16 Aug 2024 11:32:21 +0100 Subject: [PATCH] feat: add DeepThunk --- .../Multivariate/Constructions/DeepThunk.lean | 169 ++++++++++++++++++ 1 file changed, 169 insertions(+) create mode 100644 Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean diff --git a/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean b/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean new file mode 100644 index 0000000..f6d6fe4 --- /dev/null +++ b/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean @@ -0,0 +1,169 @@ +import Mathlib.Data.QPF.Multivariate.Constructions.Comp +import Mathlib.Data.QPF.Multivariate.Constructions.Prj +import Mathlib.Data.QPF.Multivariate.Constructions.Cofix +import Qpf.Macro.Comp + +namespace MvQPF + +/-! + # DeepThunk + + `DeepThunk` corresponds to the (co-)trace of a given polynomial functor. + These allows the original pfunctor to inject into them allowing for the most general state of a co-recursive principle. + + ## Stronger generaliziation + + Currently the functors are mapped as follows `F := cofix f α in α` to `DT := cofix f (β ⊕ α) in α`. + This could be generalized to `DT := cofix f ( (β ⊕ α) × (F → F) )` which would allow for modifying the returned value of a deeper call. + Note this is still a QPF as (F → F) is constant, also note the function could not be (F → DT) as this would be unproductive + (think of the function that simply skips the first value then yields a recursive construct). + This generaliziation would be useful in expression streams of for example the natural numbers as: + + codef nats : Colist ℕ := .cons 0 (nats.map Nat.succ) + + which would be productive though strange. This generalizes to nested guarded recursive structures. + Unproductive unguarded structures are limited in the same way they currently are. +-/ + +/-- + This is a fresh sum-type that represents the actions that can be taken within a `DeepThunk`. + These are that a user can either + + 1. recall - hand responsibility back to the co-recursor + 2. cont - continue constructing a DeepThunk + + These we're previously represented as a sum type but +-/ +inductive DTSum (α β : Type u) : Type u + | recall (v : α) + | cont (v : β) + +namespace DTSum +abbrev F := @TypeFun.ofCurried 2 DTSum + +def box {Γ : TypeVec 2} : F Γ → QpfSum' Γ + | recall a => MvQPF.Sum.inl a + | cont b => MvQPF.Sum.inr b + +def unbox {Γ : TypeVec 2} : QpfSum' Γ → F Γ + | ⟨i, f⟩ => match i with + | .fz => recall (f 1 .fz) + | .fs 0 => cont (f 0 .fz) + +def equiv {Γ} : F Γ ≃ QpfSum' Γ := +{ + toFun := box + invFun := unbox + left_inv := by intro x; cases x <;> rfl + right_inv := by + intro x + rcases x with ⟨(i : PFin2 _), f⟩ + dsimp only [box, unbox, Sum.inl, Sum.inr] + fin_cases i <;> { + simp only [Function.Embedding.coeFn_mk, PFin2.ofFin2_fs, PFin2.ofFin2_fz, + Fin2.instOfNatFin2HAddNatInstHAddInstAddNatOfNat, Nat.rec_zero] + apply congrArg + funext i; fin_cases i <;> (funext (j : PFin2 _); fin_cases j) + rfl + } +} + + +end DTSum + +open DTSum in +instance : MvFunctor DTSum.F where + map f x := equiv.invFun <| Sum.SumPFunctor.map f <| equiv.toFun <| x + +open DTSum in +instance : MvQPF.IsPolynomial F := + .ofEquiv _ equiv + +namespace DeepThunk +abbrev innerMapper : Vec (TypeFun (n.succ)) n := (fun + | .fz => Comp DTSum.F !![Prj 1, Prj 0] + | .fs n => Prj (n.add 2)) + +/-- The actual higher order functor taking `cofix f α in α` to `cofix f (β ⊕ α) in α` -/ +abbrev hoFunctor (F : TypeFun n) : TypeFun (n + 1) := Comp F innerMapper + +instance : MvFunctor (!![Prj 1, @Prj (n + 2) 0] j) := by + rcases j with _|_|_|_ + <;> simp only [Vec.append1] + <;> infer_instance +instance : MvQPF (!![Prj 1, @Prj (n + 2) 0] j) := by + rcases j with _|_|_|_ + <;> simp only [Vec.append1] + <;> infer_instance + +instance {i : Fin2 n} : MvFunctor (innerMapper i) := by cases i <;> infer_instance +instance {i : Fin2 n} : MvQPF (innerMapper i) := by cases i <;> infer_instance + +abbrev Uncurried (F : TypeFun n) [MvFunctor F] [MvQPF F] := Cofix (hoFunctor F) + +/-- + Between the original functor and the ⊕-composed functor there is an injection, + it occurs by taking the right step at every point co-recursively. + + The instances of the hof will have this defined as a coercion. +-/ +def inject + {F : TypeFun n.succ} {α : TypeVec n} + [inst : MvFunctor F] [MvQPF F] : Cofix F α → DeepThunk.Uncurried F (α ::: β) := + MvQPF.Cofix.corec fun v => by + let v := Cofix.dest v + + have : (hoFunctor F (α.append1 β ::: Cofix F α)) = F (α.append1 (DTSum β (Cofix F α))) := by + simp only [hoFunctor, Comp] + congr + funext i + simp only [innerMapper, TypeVec.append1] + cases i <;> rfl + rw [this] + + have arr : TypeVec.Arrow (α ::: Cofix F α) (α ::: (DTSum β (Cofix F α))) := + fun | .fz => fun a => by + simp only [TypeVec.append1] at a + simp only [TypeVec.append1] + exact .cont a + | .fs n => id + + exact inst.map arr v + +/-- + `DeepThunk.corec` is a co-recursive principle allowing partially yielding results. + It achives this by changing the recursive point to either the usual argument to the deeper call, + or continuing the structure. +-/ +def corec + {F : TypeFun n.succ} {α : TypeVec n} + [inst : MvFunctor F] [MvQPF F] + (f : β → Uncurried F (α ::: β)) + : β → Cofix F α + := (Cofix.corec fun v => by + have v := Cofix.dest v + + have : hoFunctor F (α.append1 β ::: Cofix (hoFunctor F) (α ::: β)) = F (α ::: (DTSum β (Cofix (hoFunctor F) (α.append1 β)))) := by + simp only [hoFunctor, Comp] + congr + funext i + simp only [innerMapper, TypeVec.append1] + cases i <;> rfl + rw [this] at v + + have : TypeVec.Arrow (α ::: (DTSum β (Cofix (hoFunctor F) (α ::: β)))) (α ::: Cofix (hoFunctor F) (α ::: β)) := fun + | .fz => fun | .recall x => f x | .cont x => x + | .fs _ => id + + exact MvFunctor.map this v + ) ∘ f + +end DeepThunk +/-- + `DeepThunk` is a higher-order functor used for partially yielding results in co-recursive principles. + It is defined by taking the cofix-point of the composition of the ⊕-functor and the `Base` functor. + For using this in co-recursive functions see `DeepThunk.corec` + -/ +abbrev DeepThunk (F : TypeFun n) [MvFunctor F] [MvQPF F] := DeepThunk.Uncurried F |> TypeFun.curried + +end MvQPF