The initial algebra of a multivariate qpf is again a qpf. #
For a (n+1)
-ary QPF F (α₀,..,αₙ)
, we take the least fixed point of F
with
regards to its last argument αₙ
. The result is a n
-ary functor: fix F (α₀,..,αₙ₋₁)
.
Making fix F
into a functor allows us to take the fixed point, compose with other functors
and take a fixed point again.
Main definitions #
fix.mk
- constructor- `fix.dest - destructor
fix.rec
- recursor: basis for defining functions by structural recursion onfix F α
fix.drec
- dependent recursor: generalization offix.rec
where the result type of the function is allowed to depend on thefix F α
valuefix.rec_eq
- defining equation forrecursor
fix.ind
- induction principle forfix F α
Implementation notes #
For F
a QPF, we define
fix F αin terms of the W-type of the polynomial functor
Pof
F. We define the relation
Wequivand take its quotient as the definition of
fix F α`.
inductive Wequiv {α : typevec n} : q.P.W α → q.P.W α → Prop
| ind (a : q.P.A) (f' : q.P.drop.B a ⟹ α) (f₀ f₁ : q.P.last.B a → q.P.W α) :
(∀ x, Wequiv (f₀ x) (f₁ x)) → Wequiv (q.P.W_mk a f' f₀) (q.P.W_mk a f' f₁)
| abs (a₀ : q.P.A) (f'₀ : q.P.drop.B a₀ ⟹ α) (f₀ : q.P.last.B a₀ → q.P.W α)
(a₁ : q.P.A) (f'₁ : q.P.drop.B a₁ ⟹ α) (f₁ : q.P.last.B a₁ → q.P.W α) :
abs ⟨a₀, q.P.append_contents f'₀ f₀⟩ = abs ⟨a₁, q.P.append_contents f'₁ f₁⟩ →
Wequiv (q.P.W_mk a₀ f'₀ f₀) (q.P.W_mk a₁ f'₁ f₁)
| trans (u v w : q.P.W α) : Wequiv u v → Wequiv v w → Wequiv u w
See [ACH19] for more details.
Reference #
- Jeremy Avigad, Mario M. Carneiro and Simon Hudon. Data Types as Quotients of Polynomial Functors
- ind : ∀ {n : ℕ} {F : typevec (n + 1) → Type u} [_inst_1 : mvfunctor F] [q : mvqpf F] {α : typevec n} (a : (mvqpf.P F).A) (f' : ((mvqpf.P F).drop.B a).arrow α) (f₀ f₁ : (mvqpf.P F).last.B a → (mvqpf.P F).W α), (∀ (x : (mvqpf.P F).last.B a), mvqpf.Wequiv (f₀ x) (f₁ x)) → mvqpf.Wequiv ((mvqpf.P F).W_mk a f' f₀) ((mvqpf.P F).W_mk a f' f₁)
- abs : ∀ {n : ℕ} {F : typevec (n + 1) → Type u} [_inst_1 : mvfunctor F] [q : mvqpf F] {α : typevec n} (a₀ : (mvqpf.P F).A) (f'₀ : ((mvqpf.P F).drop.B a₀).arrow α) (f₀ : (mvqpf.P F).last.B a₀ → (mvqpf.P F).W α) (a₁ : (mvqpf.P F).A) (f'₁ : ((mvqpf.P F).drop.B a₁).arrow α) (f₁ : (mvqpf.P F).last.B a₁ → (mvqpf.P F).W α), mvqpf.abs ⟨a₀, (mvqpf.P F).append_contents f'₀ f₀⟩ = mvqpf.abs ⟨a₁, (mvqpf.P F).append_contents f'₁ f₁⟩ → mvqpf.Wequiv ((mvqpf.P F).W_mk a₀ f'₀ f₀) ((mvqpf.P F).W_mk a₁ f'₁ f₁)
- trans : ∀ {n : ℕ} {F : typevec (n + 1) → Type u} [_inst_1 : mvfunctor F] [q : mvqpf F] {α : typevec n} (u v w : (mvqpf.P F).W α), mvqpf.Wequiv u v → mvqpf.Wequiv v w → mvqpf.Wequiv u w
Equivalence relation on W-types that represent the same fix F
value
maps every element of the W type to a canonical representative
Equations
- mvqpf.Wrepr = mvqpf.recF ((mvqpf.P F).W_mk' ∘ mvqpf.repr)
Least fixed point of functor F. The result is a functor with one fewer parameters
than the input. For F a b c
a ternary functor, fix F is a binary functor such that
fix F a b = F a b (fix F a b)
Equations
- mvqpf.fix F α = quotient (mvqpf.W_setoid α)
Instances for mvqpf.fix
Recursor for fix F
Equations
- mvqpf.fix.rec g = quot.lift (mvqpf.recF g) _
Access W-type underlying fix F
Equations
- mvqpf.fix_to_W = quotient.lift mvqpf.Wrepr mvqpf.fix_to_W._proof_1
Constructor for fix F
Equations
- mvqpf.fix.mk x = quot.mk setoid.r ((mvqpf.P F).W_mk' (mvfunctor.map (typevec.id ::: mvqpf.fix_to_W) (mvqpf.repr x)))
Equations
- mvqpf.mvqpf_fix = {P := (mvqpf.P F).Wp, abs := λ (α : typevec n), quot.mk mvqpf.Wequiv, repr := λ (α : typevec n), mvqpf.fix_to_W, abs_repr := _, abs_map := _}
Dependent recursor for fix F
Equations
- mvqpf.fix.drec g x = let y : sigma β := mvqpf.fix.rec (λ (i : F (α ::: sigma β)), ⟨mvqpf.fix.mk (mvfunctor.map (typevec.id ::: sigma.fst) i), g i⟩) x in have this : x = y.fst, from _, cast _ y.snd