% (find-angg "LATEX/2008projeto.tex")
% (find-dn4ex "edrx08.sty")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008projeto.tex && latex    2008projeto.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008projeto.tex && pdflatex 2008projeto.tex"))
% (find-dvipage "~/LATEX/2008projeto.dvi")
% (find-pspage  "~/LATEX/2008projeto.pdf")
% (find-dvipage "~/LATEX/2008projeto-puro.dvi")
% (find-pspage  "~/LATEX/2008projeto-puro.pdf")
% (find-pdfpage-pdftotext "~/LATEX/2008projeto-puro.pdf")
% (find-dn4ex "edrxmain41a.tex")

% (find-twupfile "LATEX/")
% (find-twusfile "LATEX/")
% http://angg.twu.net/LATEX/
% http://angg.twu.net/LATEX/2008projeto.pdf
% (ee-cp "~/LATEX/2008projeto.pdf" (ee-twupfile "/LATEX/2008projeto.pdf") 'over)
% (ee-cp "~/LATEX/2008projeto.pdf" (ee-twusfile "/LATEX/2008projeto.pdf") 'over)

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

\input 2008projeto.dnt

%
% (eedn4a-bounded)

% (eedn4a-bounded)
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")

% (eedn4a-bounded)
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")

{\bf Uma linguagem para simplificação de demonstrações:

``downcasing types''}

\msk

Eduardo Nahum Ochs

Projeto de Pesquisa

Departamento de Matemática

Pólo Universitário de Rio das Ostras - UFF

Concurso para Professor Adjunto

Rio de Janeiro / Rio das Ostras,

9 de abril de 2008

\section{Introdução}
% (find-angg "LATEX/2007dnc-sets.tex")

Tome uma prova de um enunciado geral; agora especialize-a para um caso
particular. Essa ``especialização'' funciona mais ou menos como uma
projeção: algumas distinções colapsam, alguns detalhes se perdem...

A técnica de simplificação de demonstrações na qual estou interessado
é uma espécie de processo inverso desta ``especialização''. Começamos
com uma ``prova arquetipal'' --- uma prova de um certo caso
particular, feita numa certa linguagem --- e aí {\sl mudamos o
dicionário}; a interpretação de cada termo da prova muda, e a {\sl
mesma} prova se torna uma prova do caso geral. Chamamos isto de
``levantamento''; provas arquetipais podem ser ``levantadas'' para o
caso geral, e quando isto é feito obtemos uma prova do caso geral que
usa uma linguagem herdada do caso particular arquetipal.

Estou interessado em entender melhor quatro tipos de levantamentos de
provas; a linguagem de ``downcased types'' (``DNC'', daqui por diante)
é útil para todos eles.

\msk

(1) ``Mundo funcional'' $\to$ ``Mundo lógico'' (Curry-Howard)

(2) ``Mundo real'' $\to$ ``Mundo sintático''

(3) Caso geral $\to$ caso arquetípico

(4) $\Set^\I/\F$ $\to$ Análise não-standard.

\msk

\subsection{``Mundo funcional'' $\to$ ``Mundo lógico'' (Curry-Howard)}

Compare a prova abaixo à esquerda, em Dedução Natural, de que $Q¶R$
implica $P´Q¶P´R$, com a construção do termo
$ðd¨A{×}B.\ang{d,f('d)}:(A{×}B \to A{×}C)$ em $ð$-cálculo simplesmente
tipado:

%:&\&
%:&´
%:×{×}
%:<\langle 
%:>\rangle 
%:
%:     f¨B->C                 Q->R      
%:  =============(?)      ============(?)
%:  f^\#¨A×B->A×C         (P&Q)->(P&R)   
%:                                
%:  ^4-functional?        ^4-logical?   
%:  
%:           [P&Q]^1                    [d¨A×B]^1          
%:           -------                    ---------          
%:  [P&Q]^1     Q     Q¶R   [d¨A×B]^1      'd¨B     f¨B->C 
%:  -------     ----------   ---------     ---------------- 
%:     P            R          d¨A           f('d)¨C      
%:     --------------          -----------------------      
%:         P&R                      <d,f('d)>¨A×C               
%:      ----------1          ------------------------------1
%:      (P&Q¶P&R)              ðd¨A×B.<d,f('d)>:A×B->A×C
%:                                                         
%:      ^4-logical              ^4-functional                  
%:
$$\ded{4-logical} \qquad \ded{4-functional}$$

As duas têm exatamente a mesma estrutura. Isto é um exemplo do
Isomorfismo de Curry-Howard em funcionamento; ele diz que há uma
bijeção natural entre derivações em Dedução Natural e termos de
$ð$-cálculo simplesmente tipado. Repare que na árvore um $ð$-cálculo
os termos sempre crescem à medida que descemos; se usamos uma nova
notação --- ``downcased types'' --- podemos não só manter os termos
pequenos, como suprimir os tipos --- os tipos podem ser reconstruídos
``convertendo para maiúsculas'' os termos. Note que os ``conectivos''
também têm que ser convertidos: `,' convertido para maiúscula vira
`$×$', e `$\mto$' convertido para maiúscula vira `$\to$'.

%:           [a,b]^1
%:           -------
%:   [a,b]^1    b     b|->c          a :=  (a,b)
%:   -------    -----------          b := '(a,b)
%:       a           c               c := (b|->c)(b)
%:       -------------             a,c := <a,c>
%:           a,c             a,b|->a,c := ð(a,b).(a,c)
%:         ---------
%:         a,b|->a,c
%:
%:         ^4-DNC
%:
$$\cded{4-DNC} \qquad
  \begin{array}{rcl}
               b &:=& '(a,b)       \\
               c &:=& (b \mto c)(b) \\
             a,c &:=& \ang{a,c}     \\
    a,b \mto a,c &:=& ð(a,b).(a,c)  \\
  \end{array}
$$

Agrora cada barra da árvore define um novo termo a partir de termos
anteriores; isto gera o dicionário à direita... e a semântica de cada
barra passa a ser: ``se eu sei o significado dos termos acima da
barra, eu sei o significado do termo abaixo da barra'', ou: ``se eu
sei `$a$' e sei `$c$' eu sei `$a,c$'\,'', ``se eu sei `$b$' e `$b \mto
c$' eu sei `$c$'\,'', etc.

Os ``termos'' em DNC funcionam de um modo bem diferente dos termos de
$ð$-cálculo. Em DNC nós permitimos nomes longos para variáveis (por
exemplo, `$a,b$'), a distinção sintática entre variáveis e termos
não-primitivos não existe, e, aliás, sem o dicionário não é nem
possível determinar só pelos nomes de dois termos qual é ``mais
primitivo'' que o outro: por exemplo, $b \mto c$ é mais primitivo que
$c$ mas $a,b \mto a,c$ é menos primitivo que $a,c$.


% Além disso, em DNC, fica implícito que estamos usando {\sl artigos
% indefinidos} em todo lugar: {\sl um} $a$ é {\sl um} elemento de $A$,
% {\sl um} $a\mto b$ é um elemento do espaço de funções $A \to B$, e é
% uma função que leva {\sl cada} $a$ {\sl num} $b$...
% 
% Já que a ``pronúncia'' dos termos de DNC é essa, com artigos
% indefinidos, certas perguntas soam bem naturais: ``será que existe um
% $a,b \mto b,a$ natural
% 
% Em DNC soa natural perguntar algo como: 


O significado de cada termo em DNC é implícito, derivado a partir do
contexto, e não explícito como em $ð$-cálculo... Isto faz com que no
modo natural de se ``pronunciar'' termos e árvores em DNC os artigos
sejam por default {\sl indefinidos}: ``um $b\mto c$ é uma função que
leva cada $b$ num $c$'', ``um $a,b$ é um elemento de $A×B$, e é
formado por um $a$ e um $b$''... E, repare, daí faz sentido falar de
``valor (ou significado) natural para um termo com um certo nome''.
Qual é o significado natural para $a,b \mto b,a$, por exemplo? Usando
o Isomorfismo de Curry-Howard podemos converter esta pergunta em:
``$P´Q¶Q´P$ é demonstrável em Dedução Natural? Qual é a prova?'' --- e
uma vez encontrada a prova podemos convertê-la para um termo de
$ð$-cálculo...

Perguntar se ``$P´Q¶Q´P$ é demonstrável intuicionisticamente'' é o
mesmo que perguntar se existe um morfimso de $P´Q$ para $Q´P$ numa
Álgebra de Heyting livre com geradores $P$ e $Q$; perguntar se
``existe um termo cujo tipo é $A×B \to B×A$'' é perguntar se existe um
morfismo de $A×B$ para $B×A$ na categoria cartesiana fechada livre com
geradores $A$ e $B$. A diferença entre Álgebras de Heyting (``HAs'') e
Categorias Cartesianas Fechadas (``CCCs'') é que numa HA temos no
máximo um morfismo indo de um objeto dado para outro, enquanto numa
CCC podemos ter vários; para converter uma CCC numa HA precisamos
colapsar todos os morfismos com o mesmo domínio e mesmo codomínio num
só... CCC $\to$ HA é uma projeção, e os levantamentos não são
necessariamente únicos. Por exemplo, $P´P¶P´P$ é demonstrável
intuicionisticamente, mas existem quatro termos naturais indo de $A×A$
em $A×A$, não um só... uma notação em DNC não-ambígua para estes
termos seria: $(a,a'\mto a,a)$, $(a,a'\mto a',a)$, etc. --- ou seja,
neste caso não basta converter $A×A \to A×A$ para minúsculas, é
preciso distinguir as variáveis...

Daí, isto:
%
%D diagram CCC-HA-proj
%D 2Dx     100   +50
%D 2D  100 CCC   (MF)
%D 2D       |
%D 2D       |
%D 2D       v
%D 2D  +20 HA    (ML)
%D 2D
%D (( CCC .tex= \text{CCC}
%D    HA  .tex= \text{HA}
%D    CCC HA ->
%D    (MF) .tex= \text{(Mundo"funcional)} place
%D    (ML) .tex= \text{(Mundo"lógico)} place
%D ))
%D enddiagram
%D
$$\diag{CCC-HA-proj}$$
%
é uma projeção; o levantamento, mesmo não funcionando sempre de modo
não ambíguo, nos permite usar certos termos de DNC --- por exemplo, a
função ``flip'' $a,b\mto b,a$ --- sem precisar definí-los, da mesma
forma que usamos lemas simples, como $P´Q¶Q´P$, sem demonstrá-los.

Curiosamente, várias outras operações têm bons ``downcasings''. Por
exemplo, fixe um conjunto $A$; o funtor $(×B)$, que leva cada conjunto
$A$ em $A×B$, pode ser escrito em DNC como $a \funto a,b$ (pronúncia:
``o funtor que leva cada espaço de `$a$'s no espaço dos `$a,b$'s), e o
funtor $(B \to)$ pode ser escrito em DNC como $c \funto b \mto c$; a
adjunção entre eles pode ser representada pelo diagrama à direita
abaixo, que é o downcasing do diagrama à esquerda:

%D diagram adj1
%D 2Dx     100     +25      +25     +25
%D 2D 100 A×B <--| A       a,b <=== a  
%D 2D	   |       |	    -       -  
%D 2D	   |  <->  |	    |  <->  |  
%D 2D	   v       v	    v       v  
%D 2D +25  C |--> B->C	    c ==> b|->c
%D 2D
%D (( A×B A C B->C
%D    @ 0 @ 1 <-| @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 |->
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( a,b a c b|->c
%D    @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
$$\diag{adj1}$$

Podemos escrever a versão lógica disto assim:

%D diagram adj1-L
%D 2Dx     100     +25      +25     +25
%D 2D 100 A×B <--| A       P´Q <=== P  
%D 2D	   |       |	    -       -  
%D 2D	   |  <->  |	    |  <->  |  
%D 2D	   v       v	    v       v  
%D 2D +25  C |--> B->C	    Q ===> Q¶R
%D 2D
%D # (( A×B A C B->C
%D #    @ 0 @ 1 <-| @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 |->
%D #    @ 0 @ 3 harrownodes nil 20 nil <->
%D # ))
%D (( P´Q P  Q Q¶R
%D    @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
$$\diag{adj1-L}$$

No ``mundo lógico'' para checar que $P \funto P´Q$ é um funtor basta
checar que se um morfismo $P \mto P'$ existe então o morfismo $P´Q
\mto P'´Q$ --- sua imagem pelo funtor --- também existe; não
precisamos checar nem que morfismos identidade vão em identidades, nem
que os funtores respeitam composição... uma prova de que algo é um
funtor é menor no ``mundo lógico'', e para levantá-la para o ``mundo
funcional'' precisamos provar coisas extras.

\subsection{Mundo real $\to$ Mundo sintático}

Os ``proof assistants'', como Coq ou Isabelle, são baseados em
sistemas de tipos nos quais a idéia de ``prova'' e a de ``ponto de um
conjunto'' são identificadas: para cada proposição $P$ temos o
conjunto das ``testemunhas de que $P$ é verdade'', que ou é vazio ou é
um singleton; escrevendo $W[P]$ para o conjunto das testemunhas de
$P$, temos $W[P´Q] = W[P]×W[Q]$ e $W[P¶Q] = W[P] \to W[Q]$.

Se tentamos formalizar ``funtor'' num proof assistant vemos que um
funtor $F: \catA \to \catB$ tem quatro componentes:

\msk

  * a sua ação nos objetos;

  * a sua ação nos morfismos;

  * uma prova de que ele leva identidades em identidades;

  * uma prova de que ele respeita composição.

\msk

As duas últimas componentes são a ``parte P'' do funtor (de
``provas''/``proposições''); as duas primeiras são a ``parte T'' (de
``termos'', e ``tipos'').

Podemos {\sl definir} um ``mundo sintático'' na qual a definição de
funtor só tem a parte T; idem para a definição de categoria ---
jogamos fora as equações $f¢\id = f$, $\id¢f = f$, $(f¢g)¢h = f¢(g¢h)$
---, idem para transformações naturais, etc.

Durante o meu doutorado eu imaginava que eu poderia provar algo sobre
casos em que demonstrações no ``mundo sintático'' sobre fatos básicos
de categorias se levantariam automaticamente para o ``mundo real'';
isto é, as ``condições de funtorialidade'' de um funtor se provariam
automaticamente. Hoje em dia eu vejo que esse ``mundo sintático'' é
interessante mesmo sem que o levantamento seja automático: provas em
categorias se fatoram atráves de uma projeção no mundo sintático, de
um modo que ainda não consegui formalizar totalmente.


\subsection{Caso geral $\to$ caso arquetípico}

\def\CCCL  {Ð{CCC}_{ÐL}}
\def\CCCF  {Ð{CCC}_{ÐF}}
\def\BiCCCL{Ð{BiCCC}_{ÐL}}
\def\BiCCCF{Ð{BiCCC}_{ÐF}}
\def\Hyp   {Ð{Hyp}}
\def\Toposm{Ð{Topos}_-}
\def\Toposp{Ð{Topos}_+}
\def\SetDTT{Ð{Set}_{Ð{DTT}}}

\def\M#1{\begin{matrix}#1\end{matrix}}
\def\quo#1{\text{`$#1$'}}
\def\comma{\quo,}
\def\comma{\ang,}
\def\comma{(,)}
\def\setform{\{|\}}
\def\subst{¯{subst}}
\def\pb{¯{pb}}
\def\LST{Ð{LST}}
\def\ZFC{Ð{ZFC}}

Da mesma forma que um anel é um conjunto no qual podemos interpretar
$(0, 1, +, ·, -)$, e em que estas operações se comportam ``como
deveriam'' --- isto é, certas equações são obedecidas; vamos imaginar
que uma operação só pode receber o nome `$+$' se ela ``merece este
nome'', i.e., se este `+' obedece certas equações pré-definidas ---
uma HA é uma estrutura (uma categoria) na qual podemos interpretar
$(§,´,,¶,®)$, uma hiperdoutrina é uma estrutura na qual podemos
interpretar lógica de 1ª ordem com igualdade, e um topos é uma
estrutura na qual podemos interpretar ``Local Set Theory'' ([Bell]),
que é um pouco mais que lógica de 1ª ordem com igualdade...

O diagrama abaixo mostra alguns tipos de estruturas, à esquerda, e à
direita as operações que podem ser interpretadas nelas (suas
``linguagens internas''). As setas verticais são ``especializações'';
a bijeção $\Toposm \bij \Toposp$ diz que as duas definições de topos
--- uma com só quatro axiomas, a outra com uma operação para cada
conectivo, quantificador, etc --- são equivalentes; as diagonais
pontilhadas são as projeções do isomorfismo de Curry-Howard, que mudam
os conectivos.

%D diagram basic-catsem
%D 2Dx     100    +30   +20    +20  +25    +30   +30   +30  
%D 2D  100                  CCC_F                    2CCC_F   
%D 2D                  <---  |	                <---  |	    
%D 2D  +10       CCC_L       |	         2CCC_L       |	    
%D 2D              |         v	            |         v	    
%D 2D  +20         |       BiCCC_F          |       2BiCCC_F  
%D 2D              v   <---  |	            v   <---  |	    
%D 2D  +10      BiCCC_L      /	        2BiCCC_L      /	    
%D 2D                 \     /	               \     /	    
%D 2D                  v   v	                v   v	    
%D 2D  +30              Hyp	                 2Hyp	    
%D 2D                    |	                  |	    
%D 2D                    v	                  v	    
%D 2D  +30 Topos- <--> Topos+	   2Topos- <--> 2Topos+	    
%D 2D         |          |	       |          |	    
%D 2D         |          v	       |          v	    
%D 2D  +30     \       Set_DTT	        \       2Set_DTT	    
%D 2D           \     /		         \     /		    
%D 2D            v   v		          v   v		    
%D 2D  +30        Set                      2Set               
%D 2D
%D (( CCC_L   .tex= \CCCL
%D    CCC_F   .tex= \CCCF
%D    BiCCC_L .tex= \BiCCCL
%D    BiCCC_F .tex= \BiCCCF
%D    Hyp     .tex= \Hyp
%D    Topos-  .tex= \Toposm
%D    Topos+  .tex= \Toposp
%D    Set_DTT .tex= \SetDTT
%D    Set     .tex= \Set
%D ))
%D (( 2CCC_L   .tex= (§,´,¶)
%D    2CCC_F   .tex= (*,\comma,\mto)
%D    2BiCCC_L .tex= (§,´,,¶,®)
%D    2BiCCC_F .tex= (*,\comma,÷,\mto,®)
%D    2Hyp     .tex= \M{(*,\comma,÷,\mto,®)\\(§,´,,¶,®)\\(Î,ý,=,\subst)}
%D    2Topos-  .tex= (*,\pb,\mto,\setform)
%D    2Topos+  .tex= \LST
%D    2Set_DTT .tex= \SetDTT
%D    2Set     .tex= \ZFC
%D ))
%D ((       CCC_L    CCC_F   #  0 1
%D         BiCCC_L  BiCCC_F  #  2 3
%D                Hyp        #   4
%D    Topos-    Topos+       # 5 6
%D              Set_DTT      #   7
%D           Set             #  8
%D    @ 0 @ 1 <.
%D    @ 0 @ 2 -> @ 1 @ 3 ->
%D    @ 2 @ 3 <.
%D    @ 2 @ 4 -> @ 3 @ 4 ->
%D    @ 4 @ 6 ->
%D    @ 5 @ 6 <->
%D    @ 5 @ 8 -> @ 6 @ 7 -> @ 7 @ 8 ->
%D ))
%D ((       2CCC_L    2CCC_F   #  0 1
%D         2BiCCC_L  2BiCCC_F  #  2 3
%D                2Hyp         #   4
%D    2Topos-    2Topos+       # 5 6
%D              2Set_DTT       #   7
%D           2Set              #  8
%D    @ 0 @ 1 <.
%D    @ 0 @ 2 -> @ 1 @ 3 ->
%D    @ 2 @ 3 <.
%D    @ 2 @ 4 -> @ 3 @ 4 ->
%D    @ 4 @ 6 ->
%D    @ 5 @ 6 <->
%D    @ 5 @ 8 -> @ 6 @ 7 -> @ 7 @ 8 ->
%D ))
%D enddiagram
%D
$$\diag{basic-catsem}$$

A prova de qualquer uma destas equivalências entre ``categorias com
certas estruturas extras'' e ``modelos para uma certa linguagem'' é
técnica, longa, e difícil... mas usando DNC é possível simplificar
estas provas bastante. O topos arquetípico é $\Set$; idem para a
hiperdoutrina arquetípica, a CCC arquetípica, etc. As provas em DNC
podem ser feitas usando a notação de $\Set$ e daí levantadas para o
caso geral; os diagramas em DNC permanecem os mesmos, mas se usarmos o
dicionário para expandir cada construção o resultado são expressões
que só usam as operações categóricas.

\bsk

Toposes e hiperdoutrinas também são usados para construir modelos para
linguagens que não podem ser interpretadas consistentemente em $\Set$
--- por exemplo, análise não-standard (infinitesimais numa
ultrapotência de $\Set$), geometria diferencial sintética
(infinitesimais nilpotentes), e polimorfismo (). Em todos estes casos,
curiosamente, a notação em DNC continua funcionando --- a linguagem
passa a falar de uma categoria de conjuntos com algumas operações a
mais.


\subsection{Análise Não-Standard}

% (find-angg "LATEX/2008filterp.tex")

\def\aw{{\textstyle \frac{a}{Ï}}}

Um modo de provar que $\lim_{n \to +} (1 + \frac{a}{n})^n = e^a$, em
análise não-standard, é provar que para qualque número natural
infinitamente grande $Ï$ temos $(1 + \aw)^{Ï} \sim e^a$; os passos da
prova são os abaixo:

\begin{align*}
  \log \, (1 + \aw)^{Ï}
        & = Ï \; \log\, (1 + \aw)                            \\
        & = Ï \; (\log 1 + ((\log' 1) + \o) \; \aw)        \\
        & = Ï \; (0 + (1 + \o) \; \aw)                     \\
        & = Ï \; (1 + \o) \; \aw                           \\
        & = (1 + \o) \; a                             \\
        \\
  (1 + \aw)^{Ï} & = e^{((1 + \o) \; a)}    \\
                      & = e^{(a + \o a)}      \\
                      & = e^{(a + \o')}        \\
                      & = e^a + \o''.           \\
\end{align*}

Em alguns destes passos novos símbolos --- $\o, \o', \o''$ --- são
introduzidos; seus nomes (`o'-zinhos) indicam que eles são
infinitesimais, e há quantificadores implícitos: ``existe um único
valor para $\o$ (ou $\o'$, ou $\o''$) que faz a igualdade valer''.

% (find-LATEX "2005oct20-seminar.tex" "language-tricks-1")
% (find-dn4grep "grep -nH -e place $(find *)")
% (find-dn4file "experimental.lua")
% (find-THfile "")
% (find-THfile "2007dnc-sets.blogme")


\section{O projeto}


\bsk


\section*{Referências}

[Bell]: Bell, J.L. Toposes and Local Set Theory, Oxford, 1988.

[Jacobs]: Jacobs, B. Categorical Logic and Type Theory, Studies in
Logic and the Foundations of Mathematics 141, North Holland, Elsevier,
1999.

[Pitts]: Pitts, A.M. Polymorphism is Set Theoretic,
Constructively. Springer Lecture Notes In Computer Science, vol.
283, pp. 12--39, 1987.

[Reynolds]: J. Reynolds. Polymorphism is not settheoretic. In Kahn,
McQueen and Plotkin (editors), Symposium on semantics of data types,
Volume 173 of Lecture Notes in Computer Science. Springer Verlag,
1984.

[Robinson]: Robinson, A. Non-standard analysis, Revised edition,
Princeton University Press, 1976.

[SeelyHyp]: Seely, R.A.G. Hyperdoctrines, natural deduction and
the Beck condition. Z. Math. Logik Grundlag. Math. 29 (1983), no. 6,
505--542.

[SeelyPLC]: Seely, R.A.G. Categorical semantics for higher order
polymorphic lambda calculus. J. Symbolic Logic 52 (1987), no. 4,
969--989.

[S/L]: Stroyan, K., e Luxembourg, W.A.J. Introduction to the Theory of
Infinitesimals. Academic Press, 1976.

[Wadler]: Wadler, P. Theorems for free! 4th International
Conference on Functional Programming and Computer Architecture,
London, September 1989.

%

\end{document}

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