Least fixed point containers
TODO: Make least fixed points of containers.
Here are some old notes:
Idag har jeg brukt dagen til å forstå indexed containers, en kombinatorisk beskrivelse av morfier Set/A → Set/B. Observasjoner: Man bør se på Set/A og Set/B heller som A → Set og B → Set. Det mest interessante ved disse er fikspunktene i de tilfellene hvor A = B.
For eksempel kan Fin : ℕ → Set gis som minste fikspunkt av transformasjonen T : (ℕ → Set) → (ℕ → Set) gitt ved T(F) 0 = 0 og T(F)(n+1) = F n + 1.
Observasjon: Hvis A = B = Set, så kan man, fra en transformasjon T : (Set → Set) → (Set → Set), på formen T(F)(X) = ∑ (s : S X) ∏ (p : P X s) F (N X s p) få et fikspunkt μT : Set → Set.
Eksempel: λ-kalkylefunktoren Λ : Set → Set er et fikspunkt av en transformasjon på denne formen.
Spørsmål: Når er det resulterende fikspunktet μT en beholder?
Tilstrekkelig:
S : Set
P, T : S → Set
U : (s : S) → T s → Set
V : (s : S) (t : T s) → U s t → Set
C = [S ⊲ P]
R X (s,φ) = T s
N X (s,φ) (t,ψ) = [U s t ⊲ V s t] X
T F X = ∑s ((Ps⇒X)×∏t F(∑u (Vstu⇒X)))
T (A⊲B) X = ∑ (s : S) ∑ (f : Ts → A) (g : (t : Ts) → B (f t) → U s t)
⊲ (λs f g. (Ps + ∑(t : Ts) ∑ (b : B (f t)) V s t (g t b)) ⇒ X)
Dette løser ligninger på formen:
F = μF.TF
= μF.λX. ∑s ((Ps⇒X)×∏t F(∑u (Vstu⇒X)))