|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: