nu x. a * x = a ^ (mu x. 1 + x) nu x. a * x^2 = a ^ (mu x. 1 + 2*x) nu x. a * x^b = a ^ (mu x. 1 + b*x)Lift 'em.
(nu f. \x-> x*f x) a = a ^ (mu x. 1 + x) (nu f. \x-> x*(f x)^2) a = a ^ (mu x. 1 + 2*x) (nu f. \x-> x*(f x)^b) a = a ^ (mu x. 1 + b*x)Thorsten's trick.
(nu f. \x-> x*f^2 x) a = a ^ (mu x. 1 + x^2)The generalised Thorsten trick ("polynomial").
(nu f. \x-> x * f x * f^2 x) a = a ^ (mu x. 1 + x + x^2) (nu f. \x-> x * f x * ... * f^n x) a = a ^ (mu x. 1 + x + ... + x^n) (nu f. \x-> x^c0 * (f x)^c1 * ... * (f^n x)^cn) a = a ^ (mu x. c0 + c1*x + ... + cn*(x^n))Using exponential notation [1] on the left
a ^ (nu f. 1 + f + .. + f^n) = a ^ (mu x. 1 + x + ... + x^n)(There is too much overloading of "^" to do it with coefficient types.)
-- (nu f. \x-> x * f (f x)) y = y ^ (mu x. 1 + x^2)
data A x = A_case x (A (A x)) data B = L | Sp B B a_app :: A x -> B -> x -- both typings ... a_lam :: (B -> x) -> A x -- ... are necessary a_app (A_case x stuff) = \t-> case t of L -> x Sp tl tr -> a_app (a_app stuff tl) tr a_lam f = A_case (f L) (a_lam (\tl->a_lam (\tr->f (Sp tl tr))))There seems to be another isomorphism:
a_app' (F_case x stuff) = \t -> case t of L -> x Sp tl tr -> a_app' (a_app' stuff tr) tl a_lam' f = A_case (f L) (a_lam' (\tl->a_lam' (\tr->f (Sp tr tl))))An unexpected way to update a function.
update :: A x -> B -> x -> A x update (A_case x f) t y = case t of L -> A_case y f Sp tl tr -> A_case x (update f tl (update (a_app f tl) tr y))
-- (nu f. \x-> x * f x * f (f x)) y = y ^ (mu x. 1 + x + x^2)
data G x = G_case x (G x) (G (G x)) (G (G (G x))) data H = H0 | H1 H | H2 H H | H3 H H H g_app :: G x -> H -> x g_lam :: (H -> x) -> G x g_app (G_case x gx ggx gggx) = \h-> case h of H0 -> x H1 h -> g_app gx h H2 hl hr -> g_app (g_app ggx hl) hr H3 hl hm hr -> g_app (g_app (g_app gggx hl) hm) hr g_lam f = G_case (f H0) (g_lam (\h->f (H1 h))) (g_lam (\hl->g_lam (\hr->f (H2 hl hr)))) (g_lam (\hl->g_lam (\hm->g_lam (\hr->f(H3 hl hm hr)))))
-- (nu f. \x-> x * (f (f x))^a) y = y ^ (mu x. 1 + a * x^2)
data J a x = J_case x (a -> J a (J a x)) data K a = Kl | Ks a (K a) (K a) j_app :: J a x -> K a -> x j_lam :: (K a -> x) -> J a x j_app (J_case x f) = \t -> case t of Kl -> x Ks a tl tr -> j_app (j_app (f a) tl) tr j_lam f = J_case (f Kl) (\a -> j_lam (\tl -> j_lam (\tr -> f (Ks a tl tr))))
{- (nu f (* 3 place *). \ x y z-> x^3*y*z*(f (f x x z) (f x z y) (f z y x))) a b c ~= (a, b, c) => mu (x,y,x) . ( 3 + x*x + x*y + y*x + z*z , (* occs of x *) 1 + y*z + z*y, (* occs of y *) 1 + x*z + y*y + z*x) (* occs of z *) where (a,b,c)=>(d,e,f) abbreviates a^d * b^e * c^f -}It should be noted that the constructors in the inductively defined types below
Mx, My, Mz
are systematically named
with digit-strings that represent the position of a variable name
in the the right-hand side of the definition of N
.
data N x y z = C x x x y z (N (N x x z) (N x z y) (N z y x)) data Mx = C1 | C2 | C3 | C6_1_1 Mx Mx | C6_1_2 Mx My | C6_2_1 My Mx | C6_3_3 Mz Mz data My = C4 | C6_2_3 My Mz | C6_3_2 Mz My data Mz = C5 | C6_1_3 Mx Mz | C6_2_2 My My | C6_3_1 Mz Mx -- isos ntomx :: N x y z -> Mx -> x ntomy :: N x y z -> My -> y ntomz :: N x y z -> Mz -> z mton :: (Mx -> x, My -> y, Mz ->z) -> N x y z mton (fx,fy,fz) = C (fx C1) (fx C2) (fx C3) (fy C4) (fz C5) (mton (\mx1->mton (\mx2->fx (C6_1_1 mx1 mx2), \my2->fx (C6_1_2 mx1 my2), \mz2->fz (C6_1_3 mx1 mz2)), \my1->mton (\mx2->fx (C6_2_1 my1 mx2), \my2->fz (C6_2_2 my1 my2), \mz2->fy (C6_2_3 my1 mz2)), \mz1->mton (\mx2->fz (C6_3_1 mz1 mx2), \my2->fy (C6_3_2 mz1 my2), \mz2->fx (C6_3_3 mz1 mz2)))) ntomx (C x1 x2 x3 y z n_nnn) mx = case mx of C1 -> x1 C2 -> x2 C3 -> x3 C6_1_1 mx1 mx2 -> ntomx (ntomx n_nnn mx1) mx2 C6_1_2 mx1 my2 -> ntomy (ntomx n_nnn mx1) my2 C6_2_1 my1 mx2 -> ntomx (ntomy n_nnn my1) mx2 C6_3_3 mz1 mz2 -> ntomz (ntomz n_nnn mz1) mz2 ntomy (C x1 x2 x3 y z n_nnn) mx = case mx of C4 -> y C6_2_3 my1 mz2 -> ntomz (ntomy n_nnn my1) mz2 C6_3_2 mz1 my2 -> ntomy (ntomz n_nnn mz1) my2 ntomz (C x1 x2 x3 y z n_nnn) mx = case mx of C5 -> z C6_1_3 mx1 mz2 -> ntomz (ntomx n_nnn mx1) mz2 C6_2_2 my1 my2 -> ntomy (ntomy n_nnn my1) my2 C6_3_1 mz1 mx2 -> ntomx (ntomz n_nnn mz1) mx2Note that digit-string is a position in a type expression, which has a tree structure. Styimulated by this Martin Wehr has the idea that one can "lift" the same idea to the level of types, where in general the type expressions can be coinductively defined, and the positions can be arbitrary concrete data structures. I find it hard to say where this might lead. Martin has a strong intuition of the general process, though I think he finds it hard to give a "closed form" description of it.
-- coinductive dt's data F x = C (F (G x)) x data G y = D y (F y) (G (G y)) -- inductive dt's data Fd = C1_f_g Fd Gd | C2 data Gd = D1 | D2_f Fd | D3_g_g Gd Gd -- We define the simultaneous isomorphisms by mutual recursion f_form :: (Fd -> a) -> F a g_form :: (Gd -> b) -> G b f_form fa = C (f_form (\fd-> g_form (\gd-> fa (C1_f_g fd gd)))) (fa C2) g_form ga = D (ga D1) (f_form (\fd-> ga (D2_f fd))) (g_form (\gd-> g_form(\gd'-> ga (D3_g_g gd gd')))) -- The reverse is defined again by mutual recursion f_addr :: F a -> Fd -> a g_addr :: G b -> Gd -> b f_addr (C fgx x) fad = case fad of C1_f_g fd gd -> g_addr (f_addr fgx fd) gd C2 -> x g_addr (D y fy ggy) gad = case gad of D1 -> y D2_f fd -> f_addr fy fd D3_g_g gd gd' -> g_addr (g_addr ggy gd) gd' {- Martin's explanation. (\nu F + G. \lambda X. FG X * X |\lambda Y. Y * F Y * G^2 Y) A|B ~= (\mu X + Y. X*Y | 1+ X + Y^2) => A | B where I use notation (F + G)A|B ~= C+D => A |B as abreviation of the two simultanious isomorphisms F A ~= A^C AND G B ~= B^D -}
a ^ (nu f. mu g. 1 + f * g) = a ^ (mu x. nu y. x * y)[Probably not (?) the obvious alternative
a ^ (nu f, g. f * g) = a ^ (mu x, y. 1 + x * y)because
(mu x, y. 1 + x*y) = mu x. 1 + x^2
]
If I understand the word "regular" (as used by Richard Bird),
regular datatypes are gotten from polynomial functors by closing under
(least?) fixed points.
(nu ?? ) f a = a ^ M f
where M f = mu g.\x-> x + f (g x)
.
CBT1 = mu x. 1 + x^N
CBT2 = mu x. 1 + Str x
nu ?? = a ^ CBT
(nu D. \ x -> x * (D (D x)^b)) y
isomorphic to
some function space y ^ ??
?
nu x. (Sigma a : A)x ^ B a = ??"Andreas (who just joined me) found a possible solution to your problem using two interleaved very dependent types:
{ f | f : {l | l : mu X.1 + B(f(l))} -> A }"
nu Phi. \P->P \cap (Phi^2
P)
applied to an arbitrary predicate
X
. (Predicates over some state-space S
).
This is analogous to the type functor nu F. \x->x * F^2
x
. (Just replace types by type-valued functions, ie. predicates.) The former is to the latter as ?? is to x ^ mu p. 1 +
p^2
. What would it take for this "ratio" to have a solution?
A, B, C, d
as in Petersonn-Synek trees
?? nu .. x .. a ..?? = x ^ ((mu P : A -> Set. \a-> (Sigma b : B a, Pi : C a b)P(d a b c)) a)
(nu P : A -> Set. \a-> (Pi b : B a, Sigma : C a b)P(d a b c))crops up in the type of certain kinds of "reactive strategy". If one thinks of the equations above as analyses of their left hand sides using well-founded induction (and function spaces), can one give such an analysis of this predicate? (I would be very interested in this.)
The "infinite terms" used by various proof-theorists have a stream-like, coinductive flavour which emerges when one looks at how the recursor in Gödel's T is translated. Maybe it is possible to generalise these systems of infinitary terms, so as to handle directly more general kinds of concrete data-types?
First, here is the isomorphism between streams and functions on the natural numbers.
Str x = Case_Str x (Str x) Nat = Z | S Nat lam_Str :: (N -> a) -> Str a app_Str :: Str a -> N -> a lam_Str f = Case_Str (f Z) (f . S) app_Str (Case_Str x xs) n = case n of Z -> x S p -> app_Str xs pOne usually writes
(xs !! n)
instead of app_Str xs n
.
R' : A -> Str (A -> A) -> Str A R' a (b:bs) = a : R' (b a) bs -- co R : A -> (N -> A -> A) -> N -> A R a bf n = case n of 0 -> a S m -> bf p (R a bf p) R a bf n = R' a (lam_Str bf) !! nCumulative product ((*) = flipped composition) and sum (lifted (*))
cump : Str (A -> A) -> Str (A -> A) cump (b:bs) = id : map (b*) (cump bs) -- * is exp. notn. cums : Str ((A -> A)->A->A) -> Str ((A -> A)->A->A) cums (b:bs) = zero : map (b+) (cums bs) -- * is exp. notn. where zero flip constThen
R a (bs!!) n = (cump bs !! n) a
Then, one can try to figure out the metatheory of such systems, using whatever principles on the meta-level. (The usual dreary things: church-rosser, subject reduction, ...)
One can also try to find models of such systems, which can be constructed within (well-founded) type theory. (Comparable to Aczel's graph-theoretic models of non-well-founded set-theory. Anton and I came to feel while writing our paper that we should really be developing a (type-)theory of graphs. Perhaps this is not a routine reworking of the classical theory.)
For me, the interest of all this is connected with interactive programming in type theory.
Is the direction of this "justification" reversible? (Suggested by the corecursive simulation of natrec, in the infinitary terms stuff. )
a ^ b = b a a ^ (b * c) = (a ^ b) ^ c a ^ (b + c) = a ^ b * a ^ c a ^ 0 = id
The following may not be relevant, but for the moment I think there is a chance. It was pointed out to me by Conor McBride.
B = 1 + B^2If we remove a single (not necessarily immediate) subtree from a binary tree, we are left with a structure on type
P
,
where
P = 1 + 2*B*P
n
-ary wellfounded trees:
T = 1 + T^nand we remove a single (not necessarily immediate) subtree from such a tree, we are left with a structure on type
Q
,
where
Q = 1 + n*T^(n-1)*Q
D(S*T) = S*D(T) + D(S)*T
, but for the moment, I cannot
recall exactly how.)