[pt] Considere os seguintes dois tipos de transformções em
demonstrações: 1) tornar uma prova mais incompleta,
apagando um lema ou uma construção que sejam parte da prova
e pondo no lugar um aviso dizendo isso é óbvio; 2) pegar um
passo que foi provado por um isso é óbvio, aplicar algum
algoritmo que encontre uma demonstração para esse passo, e
trocar o aviso pela demonstração de verdade. Nós vamos
considerar que a primeira operação vai em direção ao
esqueleto da demonstração, e que ela é como uma projeção;
a segunda operação é um levantamento de um esqueleto para
uma demonstração um pouco mais completa com aquele
esqueleto. Nós só estamos interessados em esqueletos que
possam ser levantados até provas completas usando algum
algoritmo conhecido. Nesta tese descrevemos uma linguagem -
o sistema DNC - que permite provar vários fatos sobre
categorias usando esqueletos. O método para o levantamento
é, a grosso modo, o seguinte: a partir do nome de um termo
em DNC nós podemos obter o seu tipo; por uma espécie de
Isomorfismo de Curry-Howard um tipo desses pode ser visto
como uma preposição numa certa lógica; um algoritmo que
obtenha uma demonstração para essa proposição retorna uma
árvore de demonstração (uma derivação) num certo sistema de
Dedução Natural, e essa árvore pode ser lida como um lambda-
termo do tipo dado - ela dá uma construção natural para um
objeto daquele tipo, e esse objeto muito frequentemente é
exatamente o objeto que esperávamos obter. Derivações em
DNC podem ser traduzidas para derivações num Pure Type
System com Dicionários (PTSD), e derivações em PTSDs podem
ser traduzidas para derivações em Pure Type Systems (PTSs);
daí, questões sobre a teoria da prova de DNC se tornam
questões sobre a teoria da prova de PTSs, que é bastante
bem-conhecida. Não só temos um levantamento de nomes de
termos em DNC para provas completas, mas também temos um
modo formal de levantar diagramas categóricos expressos na
linguagem do DNC para termos em DNC e daí para provas
completas; e se mudamos o dicionário embutido num PTSD
podemos fazer com que o mesmo esqueleto em DNC represente
provas em contextos diferentes; por exemplo, algumas provas
que aparentemente estão sendo feitas sobre a categoria dos
conjuntos podem ser reinterpretados como provas sobre um
topos arbitrário. Usamos essa idéia para apresentar de uma
forma simples - em que os passos óbvios omitidos são óbvios
num sentido muito preciso - a semântica categárica para
alguns PTSs, incluindo PTSs com polimorfismo e tipos
dependentes, e os PTSs para quais as derivações em DNC são
traduzidas. / [en] Consider the following two kinds of transformation on
proofs; the first is to make a a proof more incomplete, by
erasing a lemma or a construction from it and replacing it
by a tag saying this is obvious; the second kind of
transformation takes a step that is proved by a this is
obvious tag, applies some kind of prof-search algorithm to
it, and replaces the tag by a real proof for that step. We
will consider that the first operation goes toward the
skeleton towards a more complete proof that had that
skeleton as a projection. We are only interested in
skeletons can be lifted back to full proofs using some
known algorithm. In this thesis we can describe a language -
DNC - that lets us prove several categorical facts using
skeletons. The method for lifting these skeletons goes like
this: from the name of a DNC term we can obtain its type;
by a kind of Curry-Howard isomorphism a such type can be
seen as a proposition in a certain logic; proof-search for
that proposition will obtain a proof-tree for it in a
certain system of Natural Deduction, and that proof-tree
can be read as a lambda-term of given type - the proof-tree
gives a natural construction for an object of the given
type, that very often is exactly the object that we were
looking for. Derivations in DNC can be translated into
derivations in a Pure Type System with Dictionaries (PTSD),
and derivations in PTSDs can be translated into derivations
in Pure Type Systems (PTSs); so questions about the proof-
theory of DNC become questions about the proof-theory of
PTSs, whose properties are quite well-known. Also, not only
we can lift names of terms in DNC to full proofs in
different settings; for example, some proofs that
apparently are happening over the category of sets can be
reinterpreted as proofs over an arbitrary topos. We use
that idea to give a simple presentation (in which the
omitted obvious steps are obvious in a very precise sense)
of the categorical semantics for some PTSs - and that
includes PTSs into which the DNC derivations are translated.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:4645 |
| Date | 12 March 2004 |
| Creators | EDUARDO NAHUM OCHS |
| Contributors | NICOLAU CORCAO SALDANHA |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | TEXTO |
Page generated in 0.0022 seconds