|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2009-planodetrabalho.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (find-angg ".zshrc" "makebbl")
% (find-LATEX "catsem.bib")
% (find-LATEX "filters.bib")
% (defun b () (interactive) (find-zsh "makebbl 2009-planodetrabalho.bbl catsem,filters"))
% (defun b () (interactive) (find-zsh "bibtex 2009-planodetrabalho"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009-planodetrabalho.tex && latex 2009-planodetrabalho.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009-planodetrabalho.tex && pdflatex 2009-planodetrabalho.tex"))
% (defun d () (interactive) (find-dvipage "~/LATEX/2009-planodetrabalho.dvi"))
% (eev "cd ~/LATEX/ && Scp 2009-planodetrabalho.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2009-planodetrabalho.dvi")
% (find-pspage "~/LATEX/2009-planodetrabalho.pdf")
% (find-pspage "~/LATEX/2009-planodetrabalho.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2009-planodetrabalho.ps 2009-planodetrabalho.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2009-planodetrabalho.ps 2009-planodetrabalho.dvi && ps2pdf 2009-planodetrabalho.ps 2009-planodetrabalho.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvired -D 600 -P pk -o 2009-planodetrabalho.ps 2009-planodetrabalho.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2009-planodetrabalho.pdf" (ee-twupfile "LATEX/2009-planodetrabalho.pdf") 'over)
% (ee-cp "~/LATEX/2009-planodetrabalho.pdf" (ee-twusfile "LATEX/2009-planodetrabalho.pdf") 'over)
% «.bibliography» (to "bibliography")
\documentclass[a4paper,12pt]{article}
\usepackage[brazil]{babel}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amssymb,amsmath,amsthm}
\usepackage{babelbib}
\usepackage{url}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
\newcommand{\hoje}{29 de julho de 2009}
\title{Plano de Trabalho}
\author{%
Prof.\ Eduardo Nahum Ochs\\
Ciência da Computação\\
PURO -- Pólo Universitário de Rio das Ostras\\
UFF -- Universidade Federal Fluminense%
}
\date{\hoje}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\begin{document}
\maketitle
\section{Apresentação}
Este documento apresenta o plano de trabalho do professor Eduardo
Nahum Ochs, matrícula SIAPE 1669224, em conformidade com a resolução
219/2005 do Conselho de Ensino e Pesquisa da UFF.
Ele está escrito um primeira pessoa; ao invés de escrever ``o
professor Eduardo Ochs'', ``o professor'', etc., escreverei sempre
``eu''.
% {\sl Como em alguns pontos --- principalmente na descrição do
% projeto de pesquisa --- este documento precisa expôr impressões
% sobre vários caminhos possíveis e os motivos que provavelmente
% levarão à escolha de um (ou alguns) dentre estes caminhos, ele será
% escrito em primeira pessoa. Ao invés de escrever ``o professor
% Eduardo Ochs'', ``o professor'', etc, vou escrever sempre ``eu'' ---
% é muito mais natural e fluente expressar graus de certeza num texto
% em primeira pessoa que num texto em terceira.}
% A Seção~\ref{pesq} discute as atividades de pesquisa que o professor
% pretende conduzir; a Seção~\ref{ens} apresenta as propostas do
% professor relativas ao ensino; a Seção~\ref{ext} expõe os planos do
% professor na área de extensão.
\bsk
A Seção~\ref{pesq} discute as atividades de pesquisa que pretendo
conduzir; a Seção~\ref{ens} apresenta minhas propostas de atividades
em ensino; a Seção~\ref{ext} expõe meus planos na área de extensão.
% (find-books "__cats/__cats.el" "maclane")
% (find-books "__logic/__logic.el" "typetheory")
% (find-LATEX "catsem.bib" "bib-LambekScott")
\section{Pesquisa}
\label{pesq}
\subsection{Projeto de Pesquisa}
Pretendo cadastrar um projeto intitulado ``Downcasing types:
provas puramente sintáticas, a projeção de provas `reais' no
`mundo sintático' e levantamentos de provas do `mundo sintático'
para o `mundo real'\,'', que deve abarcar minhas principais
atividades de pesquisa nos 2 primeiros anos de meu estágio
probatório. Trata-se de um projeto nas áreas de Lógica
(\cite{GLT})), Teoria de Categorias (\cite{CWM}, \cite{Awodey}),
Teorias de Tipos (\cite{Kamareddine}), Semântica Categórica para
Teorias de Tipos (\cite{Jacobs}), (formalização de) Raciocínio
Diagramático (\cite{Kromer}, \cite{Jamnik}) e Assistentes de
Provas (\cite{Automath}, \cite{BertotCasteran}), com aplicações à
Teoria de Toposes (\cite{McLarty}, \cite{Johnstone},
\cite{Elephant1}), à Análise Não-Standard (\cite{Robinson66}) e à
Geometria Diferencial Sintética (\cite{Kock77}, \cite{Bell98}
\cite{Antipodes}).
\bsk
Meu projeto de pesquisa -- ``Downcasing Types'' --- é uma
continuação da minha pesquisa de mestrado e doutorado, e que
continuei desenvolvendo no período em que trabalhei fora do mundo
acadêmico (2004-2008).
Devido a particularidades da área de Teoria de Categorias (veja
\cite{Kromer}) muitos resultados sobre Categorias são
conceitualmente importantes, mas só se tornam publicáveis quando
são usados para provar teoremas novos não-triviais. Só em 2008 eu
consegui completar todos os detalhes de um primeiro resultado
realmente não-trivial: um método para traduzir contas com
infinitesimais --- feitas num fragmento da Análise Não-Standard
--- para ``contas standard'' em termos de continuidade e limites,
e submeti uma versão preliminar de um artigo (veja
\url{http://angg.twu.net/math-b.html}) para discussão na mailing
list internacional de Teoria de Categorias. A discussão que
resultou disto me levou a produzir material introdutório sobre
feixes e sobre lógica em grafos (veja a URL acima), usando as
técnicas de ``downcasing types'' para obter um ``modelo
arquetipal'' no qual todas as idéias ficassem claras, e a partir
do qual pudéssemos produzir provas para casos particulares
específicos que pudessem ser ``levantadas'' para o caso geral. Em
2008 e no início de 2009 apresentei parte destas idéias em
seminários na UFF de Niterói, no PURO-UFF, no IMPA e na PUC-Rio;
em cada uma destas instituições os pesquisadores locais se
interessavam mais por partes diferentes do que eu expunha, e todos
me falavam que certos teoremas de Teoria de Categorias, Toposes e
Feixes, que os livros dão a entender que são básicos, são
praticamente desconhecidos por aqui; no máximo algumas poucas
pessoas ouviram falar deles, mas ninguém nestas instituições tem
uma boa intuição a respeito do que estes teoremas ``realmente''
querem dizer... mesmo os livros tecnicamente mais acessíveis da
\'area parecem ser dirigidos principalmente a pessoas que têm de
algum modo acesso à ``cultura oral'' de Teoria de Categorias e
Teoria de Toposes --- o que não é o nosso caso! --- e este meu
trabalho sobre ``provas arquetipais'' para teoria de Feixes,
segundo as pessoas com quem discuti, seria extremamente
bem-vindo...
{\sl Ainda não é claro para mim como esta parte da pesquisa} ---
as provas arquetipais para os fatos básicos de teorias de feixes,
e sobre lógica em feixes --- {\sl deva ser publicada;} se como
material didático sobre um assunto que é relativamente avançado,
ou como uma aplicação (num certo sentido trivial; será que aí ela
teria que aparecer como um exemplo, brevemente, num artigo mais
técnico?) da técnica geral de ``downcasing types'', ou se ela deve
ser formalizada até os últimos detalhes e implementada num
assistente de prova (como em \cite{BertotCasteran} e
\cite{Automath})... e várias outras partes da pesquisa estão na
mesma situação: os ``downcasings'' dos fatos básicos sobre mônadas
(\cite{Schalk}), os para uma categoria na qual podemos fazer
cálculo com infinitesimais nilpotentes (\cite{Kock77}), os para o
chamado ``cálculo de frações'' numa categoria e para a
interpretação categórica das ``ultrapotências'' usadas em Análise
Não-Standard (\cite{Johnstone}, \cite{Fritz}), os para Categorias
Abelianas (\cite{CWM}), e os para Categorias Diferenciais
(\cite{SeelyDiff}, \cite{SeelyCartDiff}).
\bsk
Apesar das dificuldades para publicar sobre determinados assuntos,
que descrevi acima, os primeiros passos para começar a publicar a
minha pesquisa estão definidos. Devo terminar no segundo semestre
de 2009 um artigo sobre o método de ``downcasing types'', com pelo
menos as seguintes aplicações: categorias com produtos finitos,
Categorias Cartesianas Fechadas (\cite{LambekScott}) e
Hiperdoutrinas (\cite{LawvereAdjFo}, \cite{SeelyBeck},
\cite{Jacobs}). Em 2010 devo terminar artigos sobre downcasings
para categorias localmente cartesianas fechadas (\cite{SeelyLCCC},
\cite{Jacobs}), categorias nas quais se pode interpretar
$\lambda$-cálculo polimórfico (\cite{SeelyPLC}, \cite{Jacobs}), e
toposes (\cite{McLarty}), mas ainda não sei se estes assuntos
podem ser desmembrados em dois ou três artigos ou se devem ficam
num só; e depois disto vão vir os downcasings para feixes,
categorias de frações, ultrapotências, e para uma categoria
descrita em \cite{Kock77}, com infinitesimais nilpotentes (ver
também \cite{MoeRey}, \cite{Kock81}, \cite{BellSIA}). {\sl Um
cronograma detalhado será dado no projeto de pesquisa.}
% (find-LATEX "2008graphs.tex")
% (find-LATEX "2008sheaves.tex")
% Ao longo da realização do projeto, o professor pretende interagir
% com o Laboratório de Tecnologias e Métodos Formais (TecMF) da
% PUC-Rio, criando um vínculo interinstitucional que certamente será
% proveitoso para o PURO e para a UFF.
\subsection{Iniciação Científica}
Ao longo de 2010 e 2011 pretendo orientar um ou mais alunos de
bolsa acadêmica e/ou de iniciação científica em atividades
relacionadas ao projeto de pesquisa descrito acima.
\subsection{Desenvolvimento e Documentação de Software}
\label{software}
Pretendo terminar de documentar um programa que comecei a
desenvolver durante o meu mestrado
(\url{http://angg.twu.net/dednat4.html}), que facilita tarefas
como bater árvores de dedução em diagramas categóricos em \LaTeX.
Alguns alunos de graduação do PURO já se interessaram em usá-lo
para o tipo de árvores de dedução que eles vêem nas matérias de
Matemática Discreta e Lógica, e eu e o professor Fernando Náufel
do Amaral estamos pensando em modificar este programa para que ele
possa gerar diagramas 2D a partir de outros tipos de ``input'' que
não os atuais.
\subsection{Instalação de Software}
Para tornar as ferramentas e assuntos de pesquisa do LLaRC mas
acessíveis para os alunos do PURO pretendo conseguir que sejam
instalados os seguintes programas e sistemas nos computadores do
Pólo (inclusive os do laboratório dos alunos de graduação):
\begin{itemize}
\item Emacs (\url{http://en.wikipedia.org/wiki/Emacs}),
\item Eev (\url{http://angg.twu.net/emacs.html#short-eev-tutorial}),
\item \LaTeX (\url{http://en.wikipedia.org/wiki/LaTeX}),
\item Lua (\url{http://www.lua.org/}),
\item Maxima (\url{http://en.wikipedia.org/wiki/Maxima_(software)}),
\item GnuPlot (\url{http://en.wikipedia.org/wiki/Gnuplot}),
\item Dednat4 (\url{http://angg.twu.net/dednat4.html}).
\item Hugs (\url{http://en.wikipedia.org/wiki/Hugs}).
\item Ruby (\url{http://en.wikipedia.org/wiki/Ruby_(programming_language)}).
\item Python (\url{http://en.wikipedia.org/wiki/Python_(programming_language)}).
\item Tcl/Tk (\url{http://en.wikipedia.org/wiki/Tcl}),
\item OCaml (\url{http://en.wikipedia.org/wiki/Objective_Caml}).
\item Coq (\url{http://en.wikipedia.org/wiki/Coq}),
\end{itemize}
Obs: todos os programas acimas são não só gratuitos para
instalação e uso como são ``livres'' --- suas licenças permitem
cópia e modificação pelos usuários.
% {\sl Assistentes de provas: Coq e Isabelle; interpretadores para
% diversas linguagens: Hugs; Ruby; Python; Tcl/Tk; ML; beanshell}
% \item Os sistemas \TeX\ e \LaTeX\ de editoração eletrônica de
% documentos técnicos e científicos
% (\url{http://www.latex-project.org/});
\subsection{Seminários}
Pretendo apresentar seminários regulares no LLaRC (o Laboratório
de Lógica e Representação do Conhecimento do PURO-UFF), e
esporádicos na UFF de Niterói, na PUC-Rio e no IMPA sobre temas
avançados e básicos relacionados ao meu projeto de pesquisa, dando
continuidade aos contatos acadêmicos que estabeleci antes da minha
contratação pelo PURO.
\section{Ensino}
\label{ens}
\subsection{Disciplinas}
Estou apto a ministrar disciplinas diversas relacionadas aos
seguintes conteúdos:
\begin{itemize}
\item Cálculo I, II, III, IV;
\item Equações Diferenciais;
\item Álgebra Linear;
\item Matemática Discreta;
\item Análise Combinatória;
\item Lógica;
\item Teoria de Categorias;
\item Teoria dos Números.
% \item Linguagens de programação;
\end{itemize}
% (find-LATEX "catsem.bib" "Bootstrapping")
Além de disciplinas obrigatórias, pretendo oferecer disciplinas
optativas e orientar trabalhos de conclusão de curso nas áreas de
Lógica, Semântica, ``Domain-Specific Languages''
(\cite{LittleLanguages}, \cite{Bootstrapping}) e Linguagens
Funcionais, bem como obter credenciamento para atuar nos programas
de pós-graduação dos departamentos de Matemática e Ciência da
Computação de Niterói, ministrando disciplinas ligadas às minhas
\'areas de interesse e orientando dissertações e teses.
\subsection{Projeto de Ensino}
\label{projens}
Pretendo ministrar, começando ainda em 2009, alguns workshops sobre
como usar diversos programas interativos --- essencialmente todos os
da seção \ref{software} --- a partir do Emacs, guardando os logs num
formato que seja útil para as pessoas que vierem depois (veja
\url{http://angg.twu.net/eev-article.html}). Aos poucos vou tentar
descobrir como transformar estes workshops num projeto de ensino com
existência oficial, com conteúdos e objetivos bem-definidos,
cronogramas, etc.
% {\sl [Uma vez que as instalações dos programas nos laboratórios de
% informática do PURO tenham sido concluídas pretendo
% implementar um projeto de ensino relacionado a linguagens
% funcionais interativas (em especial Lua), interfaces textuais
% programáveis (Emacs e Eev), e ferramentas para geração de
% gráficos que possam ser controladas por interfaces textuais
% programáveis (Gnuplot).]}
\section{Extensão}
\label{ext}
\subsection{Projeto de Extensão}
O projeto de ensino da seção \ref{projens} é uma espécie de
continuação de um projeto de software livre que eu tenho desde o
fim da década de 90, e que interessa à comunidade de Software
Livre em geral.
Pretendo submeter à PROEX em 2010 um projeto de extensão
relacionado a isto.
% {\sl [Ainda em 2006, o professor pretende apresentar à PROEX um
% projeto para o desenvolvimento e implementação, no PURO, de
% cursos de extensão (básicos e avançados) sobre os sistemas
% \TeX\ e \LaTeX\ de editoração eletrônica de documentos
% técnicos e científicos (\url{http://www.latex-project.org/}).
% O público-alvo destes cursos inclui alunos e professores dos
% diversos cursos do PURO, bem como profissionais de nível
% técnico ou superior, que tenham interesse em produzir
% documentos técnicos e científicos (artigos, apostilas,
% manuais, etc.) de alta qualidade tipográfica. Esta atividade
% deverá incluir a participação de alunos bolsistas de
% extensão.]}
\vskip 2cm
\noindent Rio das Ostras, \hoje\
\vskip 2cm
\noindent Prof.\ Eduardo Nahum Ochs
\noindent Matr.\ SIAPE 1669224
\newpage
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%*
% (eedn4a-bounded)
% (find-sh0 "cd ~/LATEX/ && dvips -D 300 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvired -D 300 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvired -D 600 -P pk -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% {\myttchars
% % \footnotesize
% \normalsize
% \begin{verbatim}
% Software
% ========
% Dois fronts que se entrecruzam:
% Dednat4
% Forth/Lua --> Isabelle etc.
% A relação com o eev é um pouco mais distante.
%
% Novos teoremas
% ==============
% Infinitesimais naturais
% Formalização da idéia de levantamento?
% Traduções de contascom infinitesimais
% ND for PLC
% ND for LCCCs
%
% Distant goals
% =============
% Realizability
% Parametricity
% Differential Categories
% Property-like structures
% Calculus of variations
% Relate to Freyd's book
%
% Landmarks
% =========
% Downcasing hyperdoctines
% Formalizar liftings & archetypes
% Mundo sintático e mundo real
% \end{verbatim}
% }
%
% \newpage
%
% {\myttchars
% % \footnotesize
% \normalsize
% \begin{verbatim}
% Representações/traduções/impls/provas arquetipais
% =================================================
% Yoneda
% Mônadas
% Tradução de boa parte do CWM
% Sheaves
% Geometric morphisms
% Reyes/Zolfaghari
% \eps^2=0
% Filter-powers
% Abelian categories
%
% CFPs -> CCCs -> Hyps -> PLC -> Hask
% \-> LCCCs -> Toposes
%
% Colaborações prováveis, engatilhadas
% ====================================
% Fnaufel
% Mrac Simpson
%
% Colaborações não-óbvias
% =======================
% Valéria de Paiva
% Seely
% Petrúcio/Renata
% Veloso?
%
% Etc:
% ====
% Jibladze
% Sheaves as categories of fractions
% \end{verbatim}
% }
% «bibliography» (to ".bibliography")
% (find-es "tex" "makebbl" "nocite{*}")
% Occasionally the bibliography is to include publications that were
% not referenced in the text. These may be added with the command
% \nocite{key}
% given anywhere within the main document. It produces no text at all
% but simply informs BIBTEX that this reference is also to be put into
% the bibliography. With \nocite{*}, every entry in all the databases
% will be included, something that is useful when producing a list of
% all entries and their keys.
% \nocite{*}
% (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}
\end{document}
% (find-eapropos "coding")
% coding: latin-1-unix
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: