% (find-angg "LATEX/2010-proj-gma.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (find-angg                 ".zshrc" "makebbl")
% (defun b () (interactive) (find-zsh "makebbl 2010-proj-gma.bbl catsem,filters"))
% (defun b () (interactive) (find-zsh "bibtex  2010-proj-gma"))
% (defun b () (interactive) (find-zsh "bibtex  2010-proj-gma; makeindex 2010-proj-gma"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010-proj-gma.tex && latex    2010-proj-gma.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010-proj-gma.tex && pdflatex 2010-proj-gma.tex"))
% (eev "cd ~/LATEX/ && Scp 2010-proj-gma.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2010-proj-gma.dvi"))
% (find-dvipage "~/LATEX/2010-proj-gma.dvi")
% (find-pspage  "~/LATEX/2010-proj-gma.pdf")
% (find-xpdfpage "~/LATEX/2010-proj-gma.pdf")
% (find-pspage  "~/LATEX/2010-proj-gma.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2010-proj-gma.ps 2010-proj-gma.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2010-proj-gma.ps 2010-proj-gma.dvi && ps2pdf 2010-proj-gma.ps 2010-proj-gma.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-zsh0  "cp -v ~/LATEX/2010-proj-gma.pdf /tmp/pen/print/")
% (find-xpdfpage "/tmp/pen/print/2010-proj-gma.pdf")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2010-proj-gma.pdf" (ee-twupfile "LATEX/2010-proj-gma.pdf") 'over)
% (ee-cp "~/LATEX/2010-proj-gma.pdf" (ee-twusfile "LATEX/2010-proj-gma.pdf") 'over)

\documentclass[oneside]{article}
\usepackage[latin1]{inputenc}
\usepackage{makeidx}
\usepackage{hyperref}
% \usepackage{showidx}
% \usepackage{showlabels}
\makeindex
\usepackage{edrx08}       % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty"  -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex   % (find-dn4ex "edrxheadfoot.tex")
\begin{document}

\input 2010-proj-gma.dnt

\def\noedrxfooter{\gdef\footertext{}}


%*
% (eedn4-51-bounded)

%Index of the slides:
%\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")

% (find-LATEX "2008projeto.tex")
% (find-LATEX "2009-planodetrabalho.tex")
% (find-LATEX "2009unilog-abs1.tex")
% (find-LATEX "2009unilog-diags.tex")
% (find-LATEX "2009unilog-dnc.tex")

%   «.intro»			(to "intro")
%   «.dnc-exemplo»	        (to "dnc-exemplo")
%   «.graus»			(to "graus")

%   «.dnc-as-aux»		(to "dnc-as-aux")
%   «.real-e-sintatico»		(to "real-e-sintatico")
%   «.topos-theory»		(to "topos-theory")
%   «.feixes-e-mods»		(to "feixes-e-mods")
%   «.caderno»			(to "caderno")
%   «.resultados-curto»		(to "resultados-curto")
%   «.resultados-medio»		(to "resultados-medio")



% For "book":
\def\mychapter   #1#2{\chapter{#1}\label{#2}}
\def\mysection   #1#2{\section{#1}\label{#2}}
\def\mysubsection#1#2{\subsection{#1}\label{#2}}

% For "article":
\def\mychapter   #1#2{\section{#1}\label{#2}}
\def\mysection   #1#2{\subsection{#1}\label{#2}}
\def\mysubsection#1#2{\subsubsection{#1}\label{#2}}

\def\mysection   #1#2{\section{#1}\label{#2}}
% \def\mysection   #1#2{\chapter{#1}\label{#2}}

% This gives us a way to draw all the "standard
% erasings" of a tree from a single tree definition.
% Low-level words:
%
\def\archfull#1#2#3{#1\equiv #2:#3} \def\ARCHFULL    {\let\arch=\archfull}     
\def\archdnc#1#2#3{#1}              \def\ARCHDNC     {\let\arch=\archdnc}      
\def\archtermtype#1#2#3{#2:#3}      \def\ARCHTERMTYPE{\let\arch=\archtermtype}
\def\archterm#1#2#3{#2}             \def\ARCHTERM    {\let\arch=\archterm}     
\def\archtype#1#2#3{#3}             \def\ARCHTYPE    {\let\arch=\archtype}     
\def\rY#1{#1}                       \def\RY          {\let\r=\rY}              
\def\rN#1{}                         \def\RN          {\let\r=\rN}              
\def\ptypeY#1{#1}                   \def\PTYPEY      {\let\ptype=\ptypeY}      
\def\pytpeN#1{}                     \def\PTYPEN      {\let\ptype=\pytpeN}      
%
% High-level words:
%
\def\FULLRP{\ARCHFULL\RY\PTYPEY}
\def\FULLR {\ARCHFULL\RY\PTYPEN}
\def\FULLP {\ARCHFULL\RN\PTYPEY}
\def\FULL  {\ARCHFULL\RN\PTYPEN}
\def\TERMTYPERP{\ARCHTERMTYPE\RY\PTYPEY}
\def\TERMTYPER {\ARCHTERMTYPE\RY\PTYPEN}
\def\TERMTYPEP {\ARCHTERMTYPE\RN\PTYPEY}
\def\TERMTYPE  {\ARCHTERMTYPE\RN\PTYPEN}
\def\TERMRP{\ARCHTERM\RY\PTYPEY}
\def\TERMR {\ARCHTERM\RY\PTYPEN}
\def\TERMP {\ARCHTERM\RN\PTYPEY}
\def\TERM  {\ARCHTERM\RN\PTYPEN}
\def\TYPER {\ARCHTYPE\RY\PTYPEN}
\def\TYPE  {\ARCHTYPE\RN\PTYPEN}
\def\DNCR  {\ARCHDNC\RY\PTYPEN}
\def\DNC   {\ARCHDNC\RN\PTYPEN}




{\large

{\bf Uma linguagem para
\par simplificação de demonstrações:
\par ``downcasing types''}
\msk
\par Eduardo Nahum Ochs
\par Projeto de Pesquisa
\msk
\par Para o:
\par Concurso para Professor Adjunto do GMA/UFF
\msk
\par Submetido em:
\par Rio de Janeiro, 17 de maio de 2010
}

\bsk
\bsk
\bsk
\bsk
% \newpage


Se tentamos representar uma categoria $\catC$ formalmente ela vira uma
7-upla: $(\catC_0, \Hom_\catC, \id_\catC, ¢_\catC; \assoc_\catC,
\idL_\catC, \idR_\catC)$, onde as primeiras quatro componentes são
``estrutura'' e os últimos três são ``propriedades'' ---
$\assoc_\catC$ é a ``garantia'' de que a composição é associativa, e
$\idL_\catC$ e $\idR_\catC$ são garantias de que os morfismos
identidade são neutros para a composição à esquerda e à direita.

Vou chamar as componentes ``estrutura'' de ``parte sintática'' e as
componentes ``propriedades'' de ``parte lógica''. Uma {\sl
  protocategoria} é uma 4-upla $(\catC_0, \Hom_\catC, \id_\catC,
_\catC)$ --- só o ``esqueleto sintático'' do que uma categoria é, sem
as componentes que mencionam igualdades entre morfismos. Se quebramos
nos lugares certos as uplas que representam funtores, transformações
naturais, isomorfismos, adjunções, limites, etc, definimos
proto-funtores, proto-TNs, etc.

A operação que pega objetos e retorna os ``proto-objetos''
correspondentes funciona como uma projeção, e vou dizer que ela vai do
``mundo real'' --- onde cada objeto tem tanto uma ``parte sintática''
quanto uma ``parte lógica'' --- para o ``mundo sintático'', onde só as
partes sintáticas permanecem; as partes lógicas foram descartadas.

O oposto de {\sl projetar} é {\sl levantar}. Podemos tentar começar
com um ``proto-alguma-coisa'', $\aa^-$, no mundo sintático, e daí
tentar obter um ``(não-proto-)\allowbreak alguma-coisa'', $\aa$, no mundo real,
tal que a projeção de $\aa$ seja o $\aa^-$ original.

\msk

Muitos teoremas de Teoria de Categorias têm esqueletos sintáticos {\sl
  bem} interessantes: o esqueleto sintático de um teorema (ou de uma
definição) em Teoria de Categorias tem só as construções (a ``parte
divertida''), sem as partes que envolvem provas de que certos
diagramas comutam, de que duas operações dadas são inversas uma da
outra, etc (vamos chamar isto de a ``parte burocrática''). A ``parte
divertida'' é sempre intrinsicamente anterior à ``parte burocrática'',
em vários sentidos: as componentes da ``parte burocrática'' se referem
\`as componentes da ``parte divertida'', mas a ``parte divertida''
pode ser definida, e formalizada, por si só; temos que aprender a
``parte divertida'' primeiro, e depois a ``parte burocrática''; e
muitas vezes podemos ter uma noção suficientemente boa de um conceito
de Categorias só vendo as construções envolvidas nele --- e as
construções são exatamente a parte que a gente sempre precisa {\sl
  lembrar}; os enunciados certos da ``parte burocrática'' podem na
maior parte das vezes ser reconstruídos mais ou menos automaticamente
só a partir da parte divertida/sintática, ou a partir dela e de um
mínimo de informação extra, e as provas destes enunciados da ``parte
burocrática'' também podem ser reconstruídas mais ou menos
automaticamente, por busca num espaço finito de possibilidades...

\msk

Se conseguirmos os meta-teoremas certos sobre levantamentos --- por
exemplo algo como: ``toda proto-adjunção da forma {\sl tal}, $A^-$,
tem exatamente um levantamento, e podemos obtê-lo a partir de $A^-$
aplicando o algoritmo {\sl blá}'' --- então poderemos, nos casos em
que os meta-teoremas se aplicam, construir explicitamente apenas o
esqueleto $A^-$; os meta-teoremas cuidarão do resto sozinhos. Aí, nós,
humanos, poderemos fazer só a parte ``divertida'' e ``criativa'' do
trabalho --- construir o $A^-$, e encontrar novos meta-teoremas --- e
as ``máquinas'' (os meta-teoremas) farão as tarefas burocráticas e
tediosas para nós...

Infelizmente estes meta-teoremas são difíceis de se conseguir, e
raramente fazem tanto quanto gostaríamos; mas a idéia de obtê-los é
tão tentadora que é impossível escrever um projeto sobre este assunto
sem mencioná-la!... No entanto, se pensamos no {\sl caminho para obter
  estes meta-teoremas} vemos que algumas modificações básicas desta
idéia utópica tornam o projeto bem mais realista.

Em primeiro lugar, precisamos de exemplos suficientes de levantamentos
não-triviais para podermos examiná-los e ver que padrões eles
obedecem. Isto não é difícil --- os livros de Teoria de Categorias
estão cheios de teoremas não-triviais, e muitos deles (mas não todos,
como veremos) admitem esqueletos sintáticos a partir dos quais {\sl
  deveríamos} ser capazes de recontruir o teorema original. Para cada
teorema $T$ destes, com projeção $T^-$, temos um levantamento $T^-
\mto T$.

Em segundo lugar, uma das ferramentas que parece ser mais adequada
para criar estes meta-teoremas --- parametricidade --- só faz sentido
em universos com polimorfismo --- o que exclui o universo usual,
$\Set$, e sub-universos dele (\cite{ReynoldsPinST}). Modelos para
$ð$-cálculo polimórfico são categorias com algumas estruturas e
propriedades adicionais (\cite{SeelyPLC}), e precisamos entender como
definí-las e como interpretar tipos e termos de $ð$-cálculo
polimórfico como objetos e morfismos nelas (a ``linguagem interna''
delas)... isto também não parece nada simples quando vemos a versão
``mundo real'' das definições e demonstrações, mas os esqueletos
sintáticos de provas de semânticas categóricas --- isto é, de teoremas
da forma ``os modelos para a linguagem $L$ são exatamente as
categorias com estrutura extra tal'' --- são bastante elegantes.

{\sl Ou seja, a idéia de obter meta-teoremas passa para o segundo
  plano; a idéia de simplificar uma parte de Teoria de Categorias,
  separando a ``parte sintática'' (construções) da ``parte lógica''
  (diagram chasings), passa a ser central.}



% --------------------
% «dnc-exemplo»  (to ".dnc-exemplo")
% (sec "Downcasing types: um exemplo" "dnc-exemplo")
\mysection {Downcasing types: um exemplo} {dnc-exemplo}

O diagrama abaixo é um bom exemplo de como os downcasings funcionam.
Se temos um elemento $pÝA×B$ e uma função $f:B \to C$, então temos um
modo natural de obter um elemento de $C$: $f('p)ÝC$.

%L forths["<.>"]  = function () pusharrow("<.>") end
%L forths["<-->"] = function () pusharrow("<-->") end

%:
%:  \arch{a,b}{p}{A×B}
%:  ------------------\r{'}
%:      \arch{b}{'p}{B}         \arch{b|->c}{f}{B->C}
%:      -------------------------------------\r{\app}
%:                  \arch{c}{f('p)}{C}
%:
%:                    ^archetypal-deriv
%:
%D diagram archderivs
%D 2Dx     100         +40   +40     +30           +50
%D 2D  100                       \foo{\FULLRP}
%D 2D      
%D 2D  +50      \foo{\TERMTYPERP}            \foo{\DNCR}
%D 2D          
%D 2D  +50 \foo{\TERMR}   \foo{\TYPE}        \foo{\DNC}   
%D 2D
%D (( \foo{\FULLRP} \foo{\TERMTYPERP} ->
%D    \foo{\FULLRP} \foo{\DNCR} ->
%D    \foo{\TERMTYPERP} \foo{\TERMR} ->
%D    \foo{\TERMTYPERP} \foo{\TYPE} ->
%D    \foo{\DNCR} \foo{\DNC} ->
%D    \foo{\TYPE} \foo{\DNC} <-->
%D    
%D ))
%D enddiagram
%D
$$\def\foo#1{#1\fcded{archetypal-deriv}}
  \diag{archderivs}
$$

A árvore mais à esquerda embaixo constrói o $ð$-termo $f('p)$; a
\'arvore mais à direita é o downcasing correspondente. Na derivação de
um $ð$-termo os termos sempre crescem à medida que descemos na árvore,
e em construções grandes isto faz com que tenhamos árvores enormes,
com muita redundância.

O downcasing aparentemente só fala dos tipos dos objetos envolvidos, e
por isso os ``downcased terms'' --- vou chamá-los de ``nomes'' --- não
necessariamente crescem à medida que descemos na árvore; note que
permitimos ``nomes longos'', que não há distinção sintática entre
``variáveis'' e ``termos (não-atômicos)'', e que cada barra de uma
\'arvore ``downcased'' funciona como uma {\sl definição}. Por exemplo:
``se temos um valor para $a,b$ temos um significado natural para $b$
(o $b$ é a segunda componente do $a,b$)'', e ``se temos um valor para
$b$ e um valor para $b \mto c$ temos um significado natural para $c$
(obtido por aplicação)''. Note o uso de {\sl artigos indefinidos}
quando ``lemos em voz alta'' a árvore downcased, o que é algo que não
usual em Matemática.

\msk

Quando eu comecei a tentar formalizar este sistema, há cerca de 12
anos atrás, eu acreditava que ele deveria funcionar como um sistema
independente, e que deveria ser possível usá-lo {\sl ao invés} da
notação usual... ledo engano! Ele é tremendamente irregular, e
ambiguidades potenciais aparecem em quase toda tentativa de
representar construções interessantes nele --- um exemplo básico: se
$,':A×A \to A$ são as duas projeções e $f:A \to B$, podemos tentar
representar $$ e $'$ como $a,a' \mto a$ e $a,a' \mto a'$, mas aí
provavelmente vamos querer que as compostas se chamem $a,a' \mto b$ e
$a,a' \mto b'$... ou seja, a composição não é bem-comportada
sintaticamente!...

O modo de usá-lo que funciona bem --- e aqui entram várias idéias que
eu só tive nos últimos 3 ou 4 anos --- é usá-lo {\sl sempre} como um
sistema auxiliar. Por exemplo, a árvore ``downcased'' embaixo à
direita na figura acima tem que ser vista como uma abreviação, ou
``apagamento'', da \`arvore do topo, na qual certas informações da
\'arvore do topo foram apagadas; e {\sl apagamentos funcionam como
  projeções}, e para dar ``semântica'' à árvore embaixo à direita
acima --- isto é, para obter os $ð$-termos --- precisamos primeiro
construir a árvore completa do topo, depois apagar certas
informações...




% --------------------
% «graus»  (to ".graus")
% (sec "Graus de naturalidade e obviedade" "graus")
\mysection {Graus de naturalidade e obviedade} {graus}

O que a parametricidade diz, a grosso modo, é o seguinte: em certos
modelos, se temos um ``termo puro'' (isto é, sem constantes) de tipo
$T$, então ele obedece uma propriedade $P_T$, que só depende do tipo
$T$. Por exemplo, a única operação ``pura'' que espera um conjunto $A$
e retorna uma função $A \to A$ é a identidade. Repare que em $\Set$
não podemos formar o conjunto das operações deste tipo --- o domínio
de uma operação destas é a classe de todos os conjuntos, que é grande
demais.

{\sl Operações mais ``puras'' têm propriedades melhores.}

Boa parte dos artigos de Teoria de Categorias tem uma idéia subjacente
bem parecida com esta. Vou pegar um exemplo concreto:
\cite{SmithGalois} (que na verdade ``não é um artigo'', porque só pega
uma idéia de \cite{LawvereThesis} e torna-a mais clara). Mostra-se que
conexões de Galois são um caso particular de uma construção categórica
geral bastante elegante, e aí várias propriedades que costumavam ser
provadas uma a uma passam a ser óbvias; ao invés de provarmos algo
difícil mostramos que algo que era relativamente difícil quando visto
sob o ponto de vista certo é trivial --- mas, para tornar o artigo
aceitável também para pessoas que vêem a Matemática como uma
acumulação de verdades, prova-se também algo novo, ligeiramente
surpreendente. Mas o {\sl verdadeiro} tema central não é obter novas
verdades, e sim {\sl fazer as antigas caberem em menos espaço mental}.

\msk

Repare que da mesma forma que distinguimos termos ``puros'' dos demais
podemos distinguir operações que são funtoriais, que só envolvem
passos construtivos, etc... também podemos dar preferência às
operações e demonstrações que têm esqueletos sintáticos, ou cujos
esqueletos sintáticos têm boas representações por diagramas.




% --------------------
% «resultados-curto»  (to ".resultados-curto")
% (sec "Resultados esperados a curto prazo" "resultados-curto")
\mysection {Resultados esperados a curto prazo} {resultados-curto}

Acredito que vá ser possível terminar todos os itens abaixo em poucos
meses a partir do início ``oficial'' do projeto. Cada uma das
``traduções'' que menciono abaixo corresponde a não só uma
apresentação do (esqueleto sintático do) assunto numa linguagem
próxima da do modelo arquetipal, como também uma série de diagramas
comparando a notação do arquétipo com a notação usada no artigo
original (como nos slides finais de \cite{OchsUniLog}); ou seja, a
tradução não só torna o assunto mais acessível numa apresentação nova
como também dá chaves de leitura para os artigos originais.

\begin{itemize}

\item A tradução dos últimos teoremas de \cite{LawvereEqHyp} --- um
  dos primeiros artigos sobre hiperdoutrinas, escrito por um dos
  fundadores de Teoria de Topos --- e comparações com a notação
  correspondente em \cite{Jacobs} e \cite{SeelyBeck}.

\item Uma implementação do Lema de Yoneda --- tanto do seu esqueleto
  sintático quanto do teorema inteiro --- em Coq
  (\cite{BertotCasteran}), usando a notação diagramática de
  \cite{OchsUniLog} para os nomes dos objetos. Isto deve esclarecer
  muitos detalhes sobre como a projeção e o levantamento entre o mundo
  real e o mundo sintático devem funcionar.

\item A tradução de vários capítulos de \cite{CWM} e \cite{Awodey}.

\item A tradução do teorema principal de \cite{Kock77}, sobre como
  fazer cálculo diferencial numa categoria com um ``ring object of
  line type'', que se comporta como os reais em certos aspectos, mas
  que tem ``suficientes infinitesimais nilpotentes''. Em $\R \in \Set$
  não temos infinitesimais nilpotentes; a culpa é do terceiro
  excluído, e os bons universos com infinitesimais nilpotentes são
  toposes não-booleanos (\cite{BellSIA}, \cite{MoeRey}).

\item A tradução do capítulo sobre ``first order dependent type
  theory'' em \cite{Jacobs}. Como o axioma do classificador de
  subobjetos num topos perde o sentido quando projetado no mundo
  sintático é melhor começar por aqui antes de tentar chegar ao
  esqueleto sintático de Teoria de Toposes.

\item Uma introdução a Teoria de Categorias e Toposes para
  não-especialistas, que possa ser apresentada como minicurso curto
  (até como ``tutorial'' em congressos). A idéia do ``mundo
  sintático'' permite que evitemos quase todas as tecnicalidades e nos
  foquemos nas construções e em exemplos simples --- por exemplo, é
  fácil ver que $\Set^\bbV$, onde $\bbV$ é um certo DAG pequeno, é um
  topos não-booleano, e não é difícil mostrar como reinterpretar
  construções e provas de $\Set$ em $\Set^\bbV$ (através da
  ``linguagem interna'' de um topos). {\sl Obs:} um assunto preliminar
  \'e como interpretar $ð$-cálculo em uma categoria cartesiana
  fechada, e isto já está quase feito em \cite{OchsUniLog}.

\end{itemize}




% --------------------
% «resultados-medio»  (to ".resultados-medio")
% (sec "Resultados esperados a médio prazo" "resultados-medio")
\mysection {Resultados esperados a médio prazo} {resultados-medio}

Depois de terminar os resultados acima devo poder terminar vários
resultados nos quais eu comecei a trabalhar há anos, mas que para
poder publicá-los preciso entender bem certas técnicas de teoria de
categorias que ainda são meio incompreensíveis pra mim: (1)
caracterizar quais demonstrações em análise não-standard continuam
valendo quando passamos de uma ultrapotência para uma
``filtro-potência''; (2) boa parte da parte da teoria (básica) de
toposes que envolve feixes e morfismos geométricos pode ser
``levantada'' a partir de demonstrações que aparentemente acontecem no
``caso arquetipal'', que são toposes da forma $\Set^\bbD$, onde $\bbD$
\'e um DAG pequeno.

Vou dar os detalhes --- com figuras --- na apresentação oral do
projeto.

% (find-angg "LATEX/2007dnc-sets.tex")







% (find-LATEX "2009-planodetrabalho.tex")
% (find-LATEX "catsem.bib" "test")
% (find-LATEX "filters.bib")
% (find-zsh "makebbl 2009-planodetrabalho.bbl catsem,filters")
% (find-es "tex" "makebbl")
% \bibliographystyle{alpha}
\bibliography{catsem,filters}
\bibliographystyle{alpha}

% \printindex





%*

\end{document}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End: