% % mar99a.dn % % (find-fline "feb98.tex") % (find-fline "mar99b.dn") % (find-fline "tese2.sty") % (find-fline "Makefile") % Esse bloquinho ‚ pra parametricidade: % \Ta2\T_{a^2} \Tb2\T_{b^2} \6-a=>\ldots \6a=>\5 \5-b=>\ldots \5b=>(\4) \4(a->b)->(\2) \2a^{[]}->b^{[]} ->^{\ton{ ->\to  \/\lor  /\\land  \n\nn  pi1{\pi_1} pi2{\pi_2} RF\ruleF a{\alpha} b{\beta} c{\gamma} yP->yy|_{Pxy}->y yP->õy|_{Pxy}->õ_{Pxy} yP1[y|_{Pxy}]1 yP[y|_{Pxy}]1 []:[]  [][\;] ]1]^1 ]2]^2 \A\cpoV  \B\cpoDois  ÐÐ\Lambda  ==>\funto  &&\LAND  =>\TO  \TN\mathrm{TN} %%% % % 1.1: Um primeiro problema % %%% s s->(x->y) ------------ x->y (x->y)->(x->j) ----------------------- x->j j->L --------------------- x->L (x->L)->I ------------------------ I ^variac %%% % % 1.?: µrvores % %%% -© - - b © b © 1 1 ----/\ ---- ---- a b/\© a b/\© 1 2 ---------\to --------- ------- a->(b/\©) a->(b/\©) 3 ^formacao-com ^formacao-sem ^formacao-alt a n_1 -R --- a b n_2 n_3 ---- -R' -------- --- c b a n_4 n_5 n_6 -------- --------------- c n_7 ^demotree ^demotree-nodes %%% % % 2.1: Termos % %%% x f a a->b ---- ------- f(x) g b b->c ------- ---------- g(f(x)) c ---------- ---- Ðx.g(f(x)) a->c ^x.g(f(x)) ^x.g(f(x)).t %%% % % 2.6: As redu‡äes e a  rvore dos tipos % %%% [x]1 f [a]1 a->b ------- ---------- f(x) g b b->c -------- ---------- g(f(x)) c ----------1 ----1 Ðx.g(f(x)) a->c ^x.g(f(x)).disch ^x.g(f(x)).disch.t [x]^2 (+) [\n]^2 \n->(\n->\n) [\n_2]^2 (+) --------- ------------------- ------------ [x]^2 (+)x [\n]^2 \n->\n [\n_2]^2 (+)\n_2 ------------ --------------- ------------------ (+)x\,x \n (+)\n_2\,\n_2 ----------1 ------ -------------------1 Ðy.(+)x\,x \n->\n Ð\n_1.(+)\n_2\,\n_2 -------------2 ---------- -------------------------2 Ðx.Ðy.(+)x\,x \n->\n->\n Ð\n_2.Ð\n_1.(+)\n_2\,\n_2 ^fromtype.1 ^fromtype.2 ^fromtype.3 [x]1 g [x]1 f [a]1 a->b [a]1 a->(b->c) ------ ------ --------- -------------- gx fx b b->c ---------- --------------- y h fx(gx) d d->a c --- ---------1 ------ ----1 hy Ðx.fx(gx) a a->c --------------- --------------- (Ðx.fx(gx))(hy) c ^betared1f ^betared1t y h y h d d->a d d->a --- --- ------ ------ hy g hy f a a->b a a->(b->c) ------ ----- --------- -------------- g(hy) f(hy) b b->c ------------- ---------------- f(hy)(g(hy)) c ^betared2f ^betared2t %%% % % 2.?: Atribui‡Æo de tipos a termos nÆo-tipados % %%% ------- [a/\b]^1 a/\b->b ------- ---------------- ------------ [a/\b]^1 a/\b->a b b->(a->b/\a) ---------------- ---------------------- a a->b/\a --------------------------------- b/\a ----------1 a/\b->b/\a ^wideflip.t --- [p]1 pi2 --- --------- -- [p]1 pi1 pi2p \P --------- ------------ pi1p \P(pi2p) ------------------ \P(pi2p)(pi1p) -----------------1 Ðp.\P(pi2p)(pi1p) ^wideflip a_1 a_2 \ldots a_n ---------------------RF{C} Ca_1a_2\ldotsa_n ^rulef [a/\b]1 [a/\b]1 [p]1 [p]1 [p]1 [p]1 ------- ------- ----RF{pi2} ----RF{pi1} ---- ---- b a pi2p pi1p pi2p pi1p ---------- ----------------RF{\P} -------------- b/\a \P(pi2p)(pi1p) \P(pi2p)(pi1p) ----------1 -----------------1 -----------------1 a/\b->b/\a Ðp.\P(pi2p)(pi1p) Ðp.\P(pi2p)(pi1p) ^flip.t ^flip.fr ^flip.f %%% % % 2.?: Polimorfismo % %%% [p]2 [x/\a]2 ---- ------- [p]2 pi2p [f]1 [x/\a]2 a [a->b]1 ---- ---------- ------- ------------- pi1p f(pi2p) x b ------------------- ---------- \cbP(pi1p)(f(pi2p)) x/\b ----------------------1 --------------1 Ðf.\cbP(pi1p)(f(pi2p)) (a->b)->(x/\b) -------------------------2 ----------------------2 Ðp.Ðf.\cbP(pi1p)(f(pi2p)) x/\a->((a->b)->(x/\b)) ----------------------------- ---------------------------- ÐÐx.Ðp.Ðf.\cbP(pi1p)(f(pi2p)) x==>(x/\a->((a->b)->(x/\b))) ^polim1 ^polim2 %%% % % 3: Dedu‡Æo natural % %%% a_1 \ldots a_n ================ b ^bd0 [a]^1 a->b ---------- a a->b b b->c [a]^1 a->b b->c ------- --------- ================ b b->c a a->b b->c c c --------- ============= ----1 ----1 c c a->c a->c ^bd1 ^bd2 ^bd3 ^bd4 [a]^1 A ======== c ----1 a->c ^bd5 a b a/\b a/\b ------\andI ------\andE1 ------\andE2 a/\b a b ^andI ^andE1 ^andE2 [a] A [b] B ======= ======= a b a\/b c c ------\orI1 ------\orI2 ---------------------\orE a\/b a\/b c ^orI1 ^orI2 ^orE [a] A ======= a a->b b ----------\toE ------\toI b a->b ^toE ^toI © --\botE -\topI a õ ^botE ^topI [a] a->c [b] b->c ----------- ----------- a\/b a->c b->c a\/b c c ----------------------\orE' --------------------------\orE c c ^orE' ^orE'-tra [a]1 A [b]2 B ======= ======= c c ------1 ------2 a\/b a->c b->c -----------------------\orE' c ^orE-tra %%% % % 3.?: Normaliza‡Æo % %%% A B A B == == == == a b a b ------ ------ a/\b A a/\b B ------ == ------ == a a b b ^and-norm1 ^and-norm2 ^and-norm3 ^and-norm4 [a]1 B ======== A b A == ------1 == a a->b a B ---------- ===== b b ^to-norm1 ^to-norm2 A' == a [a]1 A [b]1 B A' ------ ======== ======== == a\/b c c a A -----------------------1 ====== c c ^or-norm1 ^or-norm2 B' == b [a]1 A [b]1 B B' ------ ======== ======== == a\/b c c b B -----------------------1 ====== c c ^or-norm3 ^or-norm4 b [ªb]1 b [ªb]1 ------- ------- [a]1 c © [a]1 c © ------- ---- ------- ---- a\/ªb a/\c a/\c a/\c a/\c -------------------- ---- ---- a/\c a\/ªb a a ---- -----------------1 a a ^cpex1 ^cpex2 b [ªb]1 ------- © b [ªb]1 ---- ------- a/\c © ---- - a\/ªb [a]1 a a\/ªb [a]1 a -----------------1 ---------------1 a a ^cpex3 ^cpex4 %%% % % 3.?: Quantificadores % %%% [x]1 A ======= õ_{íx} õ_\phi x õ_\phi --------------1:\ExE -----------\ExI õ_\phi õ_{íx.\phi} ^ExE ^ExI [x]1 A ======= x õ_{ìx.\phi} õ_\phi --------------\FaE -----------1:\FaI õ_\phi õ_{ìx.\phi} ^FaE ^FaI x õ_{ìx.ìy.(Pxy->Pyx)} -----------------------\FaE y õ_{ìx.(Pxy->Pyx)} ----------------------\FaE õ_{Pxy} õ_{(Pxy->Pyx)} -------------------------- õ_{Pxy} õ_{Pyx} ----------------------- y õ_{Pxy/\Pyx} -------------------\ExI õ_{íy.(Pxy/\Pyx)} ^praw19.1 [y|_{Pxy}]1 [y|_{Pxy}]1 ----------- ----------- [x]2 õ_{ìx.íy.Pxy} [x]2 y õ_{Pxy} õ_{ìx.ìy.(Pxy->Pyx)} -------------------\FaE =================================================== õ_{íy.Pxy} õ_{íy.(Pxy/\Pyx)} -------------------------------------------------1:\ExE õ_{íy.(Pxy/\Pyx)} --------------------2:\FaI õ_{ìx.íy.(Pxy/\Pyx)} ^praw19.2 ìx.ìy.(Pxy->Pyx) ----------------\FaE ìy.(Pay->Pya) -------------\FaE [Pab]1 Pab->Pba ----------------- [Pab]1 Pba ------------- ìx.íy.Pxy Pab/\Pba ---------\FaE -------------\ExI íy.Pay íy.(Pay/\Pya) ---------------------------1:\ExE íy.(Pay/\Pya) ----------------\FaI ìx.íy.(Pxy/\Pyx) ^praw19-orig1 ìx.ìy.(Pxy->Pyx) ----------------\FaE ìy.(Pxy->Pyx) -------------\FaE [Pxy]1 Pxy->Pyx ----------------- [Pxy]1 Pyx ------------- ìx.íy.Pxy Pxy/\Pyx ---------\FaE -------------\ExI íy.Pxy íy.(Pxy/\Pyx) ---------------------------1:\ExE íy.(Pxy/\Pyx) ----------------\FaI ìx.íy.(Pxy/\Pyx) ^praw19-orig2 [a]1 b ========= õ_{ía} õ_c ---------------1:\ExE õ_c ^admiss-ExE %%% % % 4: Categorias % %%% a->b a->b a->b b->c \O_a ------ ------ -------------- ------ \O_a \O_b a->c a->a ^crdom ^crcod ^crcomp ^crid a->^{f}b -------- \O_b ---- a->^{f}b b->b -------------- a->b ^constrboba1 a->^{f}c c->a' a->^{g}c c->a' a->b b->a' --------------- --------------- ----------- a->a' a->a' a->^{\id}a' a->a' ^cnex1 ^cnex2 ^cnex3 ^cnex4 [a]1 a->^{f}c -------------- c c->a' --------------- a' -----1 a->a' ^cn-withpoints a->b b->c a->^{f}b b->^{g}c a->^{f}b b->^{g}c ----------½ ------------------ ------------------ a->c a->^{g½f}c a->^{f}b->^{g}c ^comp1 ^comp2 ^comp3 a->b b->c f g ---------- ----½ a->b->c g½f ^comp4 ^comp5 a->b b->c f g ---------- ---- a->c g½f ^comp0a ^comp0b %%% % % 4.4: Funtores % %%% a->b b->c a->b b->c -------- -------- ---------- a^F->b^F b^F->c^F a->c ------------------ -------- a^F->c^F a^F->c^F ^functor0.a ^functor0.b g f g f --- --- ----- g^F f^F f½g --------- ------- f^F½g^F (f½g)^F ^functor0.af ^functor0.bf [i]1 [i->a]2 ------------- a a->b ------------- b ----1 i->b --------------2 (i->a)->(i->b) ^functor-exp %%% % % 4.5: Transforma‡äes naturais % %%% \O_a \O_a ---------F ----------\TN \O_{a^F} a^F->a^G ----------------\TN ----------------H a^{FH}->a^{FK} a^{FH}->a^{GH} ^tn1 ^tn2 %%% % % 4.7: Produtos % %%% x->a x->b \coneab{p} ---------------------- x->p ^prod1 a->b a->c --------------ž ----------\pi ----------\pi' a->b/\c b/\c->b b/\c->c ^prod2 ^prod2p1 ^prod2p2 a->b a->c -------------- ---------- a->b/\c b/\c->b ------------------------ a->b a->b ^prodeq1a ^prodeq1b a->b a->c -------------- ---------- a->b/\c b/\c->c ------------------------ a->c a->c ^prodeq2a ^prodeq2b a->b/\c a->b/\c ========== ========== a->b a->c ------------------ a->b/\c a->b/\c ^prodeq3a ^prodeq3b --------- a/\c->a a->b ----------------- -------- a/\c->b a/\c->c ----------------------- a/\c->b/\c ^functor-prod %%% % % 4.8: Adjun‡äes % %%% a->b b->c^L a->b ------------ -------- a->c^L a^R->b^R b^R->c ------ ---------------- a^R->c a^R->c ^adj-abc1 ^adj-abc2 b^R->c c->d c->d ------------ -------- b^R->d b->c^L c^L->d^L ------ ---------------- b->d^L b->d^L ^adj-bcd1 ^adj-bcd2 a^R->b ----------- a->a^{RL} a^{RL}->b^L ---------------------- a->b^L ^adj-bijdown a->b^L ------ a^R->b ^adj-bijup a->b ---- \O_b --------- a->b b->b^{RL} --------------- a->b^{RL} --------- a^R->b^R ^adj-functor %%% % % 4.9: O sistema CCC % %%% a->b b->c ------\id --------------½ a->a a->c ^CCCid ^CCCcomp a->b a->c --------------\andI_\CCC ----------\pi ----------\pi' a->b/\c a/\b->a a/\b->b ^CCCandI ^CCCpi1 ^CCCpi2 a->c b->c --------------\orI\CCC ----------\kappa ----------\kappa' a\/b->c a->a\/b b->a\/b ^CCCorI ^CCCk1 ^CCCk2 a/\b->c ------------\cur ----------------\ev a->(b->c) a/\(a->b)->b ^CCCcur ^CCCev -----õ_\CCC a->õ ^CCCT -----©_\CCC ©->a ^CCCbot ---------- a/\b->a a->(b->c) ---------- ------------------------ a/\b->b a/\b->(b->c) -------------------------------- ---------------- a/\b->b/\(b->c) b/\(b->c)->c ----------------------------------------------- a/\b->c ^uncur %%% % % 4.10: Limites % %%% x->a' ---------- x->(c,d,f) ------------ x->(c,d,e,f) --------------* x->(c,b,d,e,f) ---------------- x->(a,c,b,d,e,f) ---------------- x->a ^bijs-2pbs