Projeto de pesquisa: Logica Matematica, teoria

da prova e teoria de funcoes

Coordenadora: Elaine Gouvea Pimentel

Pesquisadores: Dale Miller

Simona Ronchi della Rocca

Luca Paolini

Luca Roversi

Alessio Guglielmi

Paola Bruscoli

Alunos: Mario Sergio Ferreira Alvim Junior

Vivek Nigam

Fabiana Lopes Fernandes

Carlos Salvador Murray

Giselle Machado Nogueira Reis

Henrique Antunes Almeida

Frederico Augusto Menezes Ribeiro

Joyce Figueiro

19 de novembro de 2008

1

Sumario

1 Identificacao da proposta 3

2 Qualificacao dos problemas a serem abordados 4

3 Objetivos 4

4 Organizacao do projeto 5

5 Metodologia 6

6 Revisao da literatura 66.1 PARTE I . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

6.1.1 Logica (classica) de primeira ordem . . . . . . . . . . . . 66.1.2 Logica intuicionista . . . . . . . . . . . . . . . . . . . . . . 86.1.3 Logica Linear . . . . . . . . . . . . . . . . . . . . . . . . . 106.1.4 Logica e Matematica . . . . . . . . . . . . . . . . . . . . . 116.1.5 Logica e Ciencia da Computacao . . . . . . . . . . . . . . 126.1.6 Deducao natural versus calculo de sequentes . . . . . . . . 136.1.7 Cut elimination . . . . . . . . . . . . . . . . . . . . . . . . 156.1.8 Logical frameworks . . . . . . . . . . . . . . . . . . . . . . 156.1.9 Logica Linear como framework para especificar sistemas

de sequentes . . . . . . . . . . . . . . . . . . . . . . . . . 166.2 PARTE II . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

6.2.1 λ-calculus e computabilidade . . . . . . . . . . . . . . . . 176.2.2 λ-calculus tipado simples . . . . . . . . . . . . . . . . . . 206.2.3 Sistema de tipos intersecao . . . . . . . . . . . . . . . . . 226.2.4 Isomorfismo de Curry-Howard . . . . . . . . . . . . . . . . 23

7 Principais contribuicoes cientıficas 247.1 PARTE I . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 247.2 PARTE II . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

8 Identificacao dos demais participantes do projeto 26

9 Apoios, parcerias ja estabelecidas e contrapartidas das insti-tuicoes financeiras 27

2

1 Identificacao da proposta

O presente projeto consiste, na verdade, de quatro sub-projetos de pesquisadistintos (porem relacionados entre si) que desenvolvo atualmente. Sao eles:Logica Linear, Calculo das Estruturas, Tipos Intersecao e λ-calculus.

O primeiro e o segundo sub-projetos (que chamarei de Parte I) estao dentroda area de teoria da prova.

O primeiro sub-projeto: Linear Logic and the specification of logical systemse ainda fruto do trabalho desenvolvido durante a minha tese de doutorado. Fazparte de dois projetos maiores: PARSIFAL1 e SLIMMER2 coordenado peloProf. Dale Miller (INRIA/LIX) – meu orientador de doutorado e atual cola-borador. Tal sub-projeto deu origem a um grupo de pesquisa no CNPq, lacadastrado com o nome Logica Linear e a especificacao de sistemas computaci-onais.

O segundo sub-projeto: Calculus of Structures e desenvolvido em parceriacom o grupo de Inteligencia Artificial da Universidade de Bath3. Desde a suacriacao por volta do ano 2000, o grupo tem crescido e varios alunos de mestradoe doutorado tem sido formados. Por ser uma area nova, os grandes problemasestao ainda em fase embrionaria de desenvolvimento. Deste modo, a quantidadede resultados que se pode obter a curto prazo e enorme, e o meu conhecimentode calculo de sequentes e simetria de provas tem gerado um grande interessepor parte do Prof. Alessio Guglielmi para que eu faca parte do seu grupo depesquisa. De fato, tal colaboracao ja rendeu frutos uma vez que o meu aluno demestrado (Mario Sergio Alvim) defendeu a sua dissertacao nesta area, provandoalguns novos e fascinantes resultados, que descreverei mais adiante.

Os outros dois sub-projetos (que chamarei de Parte II) nasceram durante arealizacao do meu pos-doutorado no Dipartimento di Informatica da Universitadi Torino, Italia, no perıodo de 11/2003 a 01/2005. Fazem parte da area deteoria de funcoes.

O Departamento di Informatica da UNITO e famoso por ter sido o bercoda teoria de Intersection Types nos anos 1980 e e justamente nesta area queesta inserido o terceiro sub-projeto. O projeto Intersection types and discretepolymorphism faz parte do projeto FOLLIA4, coordenado pela Profa. SimonaRonchi della Rocca (UNITO), com quem trabalhei no pos-doutorado. Alem daprofessora Simona, tambem esta inserido no projeto o professor Luca Roversi(UNITO).

Finalmente, o quarto sub-projeto: λ-calculus and strong normalization, tambemdentro de FOLLIA, tomou forma a partir da publicacao do livro [33] pelos pes-quisadores Simona Ronchi della Rocca e Luca Paolini (UNITO). Tal livro apre-senta o λ-calculus parametrico e daı surgiu a ideia de caracterizar o λ-calculuscall-by-value ou call-by-name de acordo com o conjunto de termos que podemser passados como parametro na β-reducao.

1http://www.lix.polytechnique.fr/parsifal/2http://www.lix.polytechnique.fr/Labo/Dale.Miller/slimmer/3http://www.computational-logic.org/˜guglielm/group/4http://follia.di.unito.it/index.html

3

2 Qualificacao dos problemas a serem aborda-

dos

Os resultados pretendidos na PARTE I relacionados a Logica Linear saouma continuacao do que ja foi obtido em [19, 20] e [29]. Todos os tres trabalhosforam publicados, e dois deles apresentados como invited talks em conferenciasinternacionais. O que pretendemos agora e fechar a teoria, adicionando conceitoscomo inducao sobre provas e polaridades ao que ja foi feito. E um passo muitogrande e inedito (como foram todas as tres etapas do trabalho), e um resultadode grande impacto na area de teoria da prova.

Com relacao a Calculus of Structures, como se trata de um formalismo novo,ha muito o que fazer. Ate o presente momento, definimos (eu e o aluno MarioSergio) o conceito de computacao para um fragmento da logica linear. Esseresultado e considerado relevante porque determinar quais sao os aspectos com-putacionais de um formalismo permite utiliza-lo como ferramenta para provarpropriedades de sistemas dedutivos, softwares e hardwares, por exemplo. Alemde ser um resultado teorico interessante per se. A intencao e aumentar o frag-mento de trabalho, de modo a estender o poder da ferramenta.

Na PARTE II, os resultados esperados sao baseados nos trabalhos ja re-alizados [22, 23] e [30, 31]. Novamente, o impacto teorico e grande, pois osresultados pretendidos sao relevantes para a comunidade da area de teoria daprova, e pode ter tambem aplicacoes praticas, uma vez que pretendemos proporuma linguagem logica de programacao que suporte polimorfismo discreto.

Ha de se observar que os pesquisadores colaboradores sao todos figuras derenome na area, e meus trabalhos com eles sao quase sempre apresentados emimportantes conferencias como invited talks. Isso faz com que a visibilidade dotrabalho seja grande.

3 Objetivos

Os objetivos principais da PARTE I sao:

a) provar, de forma automatica, propriedades de sistemas logicos e computa-cionais especificados utilizando como meta-logica a Logica Linear munidade definicoes e inducao. Tambem pretende-se adicionar a Logica Linear oconceito de inducao sobre provas;

b) usar Calculo de Estruturas como uma ferramenta logica para especificarsistemas de provas (tais como aqueles nao comutativos) e aprofundar noestudo de propriedades de sistemas logicos usando deep inference e sime-tria;

c) aplicar o conceito de polaridades em definicao e sistemas de prova de modoa estabelecer uma teoria nova para provar propriedades sobre a estruturade provas.

Os objetivos principais da PARTE II sao:

d) apresentar uma linguagem tipada que suporte polimorfismo discreto e sejauma decoracao da logica isomorfa aos tipos intersecao;

4

e) apresentar uma caracterizacao sintatica das funcoes fortemente norma-lizaveis em λ-calculus utilizando o sistema de tipos intersecao;

Este e um projeto dentro da area de fundamentos da matematica (logica,teoria da prova e teoria de funcoes) e teoria da computacao (linguagens deprogramacao).

4 Organizacao do projeto

PARTE I. Comecamos a revisao da literatura apresentando as logicasclassica e intuicionista, que formam a base da logica utilizada pelos matematicose a logica “construtiva”, respectivamente. A seguir, passamos a descrever aLogica Linear, que e uma logica de recursos conscientes.

A logica intuicionista e de particular interesse porque, ate o presente mo-mento, ela tem sido utilizada como ferramenta para a especificacao de sistemasde provas em deducao natural.

Ocorre que Logica Linear pode ser utilizada de maneira similar para especi-ficar sistemas de provas mais gerais baseados em calculo de sequentes. Como ascodificacoes sao naturais e diretas, podemos utilizar a rica meta-teoria de LogicaLinear para provar propriedades sobre os sistemas de prova das logicas-objeto.

Como as codificacoes das logicas-objeto resultam em programas logicos, epossıvel implementar os sistemas de prova codificados. Deste modo, varias pro-vas podem ser automatizadas e algumas propriedades dos sistemas codificadospodem ser automaticamente verificadas.

Podemos tambem caminhar na direcao oposta e apresentar meta-definicoesde sistemas logicos ideais, ou seja, apresentar uma caracterizacao de meta-especificacoes sintaticas que um sistema de provas deve possuir de modo quese possa garantir que tal sistema tenha “boas” propriedades logicas, tais comocut-elimination e restricao do axioma inicial ao caso atomico.

Mas esse tipo de argumentacao exige inducao e tambem definicoes dentroda meta-linguagem escolhida. Deste modo, a fim de aumentarmos o poder deLogica Linear como meta-logica, os conceitos de definicao e inducao devem serincluıdos a um fragmento da Logica Linear.

Ocorre que certas definicoes sao positivas, enquanto que outras sao negati-vas, dependendo dos conectivos utilizados no corpo dos predicados definidos.Desta forma, podemos provar propriedades sobre os predicados e determinar aestrutura de uma prova utilizando a nocao de polaridades.

O proximo passo seria o uso de Calculo de Estruturas (desenvolvido pelogrupo de Inteligencia Artifical da Universidade de Dresden) a fim de especificaroutros sistemas logicos e provar propriedades sobre eles, principalmente aquelesque nao podem ser representados atraves do calculo de sequentes. Alem disso,sendo o Calculo de Estruturas uma ferramenta logica que enfatiza a dualidadedentro de sistemas de prova, nos parece que tal calculo e o candidato perfeitopara fazer esse tipo de argumentacao sem estar limitado a uma estrutura logicamuito restritiva, tal como o proprio calculo de sequentes.

PARTE II. Como parte da revisao da literatura existente no assunto,comecamos por apresentar o λ-calculus, que e uma teoria que representa funcoescomo regras, ao inves da tradicional abordagem de funcoes como graficos. Essaabordagem possibilita o estudo de computabilidade de funcoes, uma vez que as

5

funcoes representaveis em λ-calculus sao exatamente as funcoes recursivamenteenumeraveis. Os termos de λ-calculus que sao fortemente normalizaveis repre-sentam as funcoes recursivamente enumeraveis cuja execucao sempre termina,independente da estrategia de reducao adotada. E sabido que a pertinencia deuma funcao nesse conjunto e indecidıvel. Entao uma caracterizacao sintaticaajuda a entender melhor de tais funcoes.

A seguir, apresentaremos o λ-calculus simplesmente tipado e o sistema detipos intersecao. Os dois calculus sao bastante parecidos, a unica diferencasendo a inclusao do tipo intersecao ∩ e das regras de inferencia para esse tipo.Essa pequena diferenca resulta em passar de um sistema decidıvel (λ-calculussimplesmente tipado) para um sistema indecidıvel (sistema de tipos intersecao– em ingles: intersection types assignment system), mas que tipa todos e exata-mente os termos fortemente normalizaveis do λ-calculus atipado. Terminandoa parte de revisao, a Secao 6.2.4 descreve a relacao entre os mundos logico ecomputacional, atraves do isomorfismo de Curry-Howard, aqui descrito para ocaso: logica intuicionista/λ-calculus.

Apos a revisao, sera apresentado do projeto em si, com a justificativa deporque penso que este projeto seja de relevancia para a pesquisa na area delogica/fundamentos de matematica/computacao teorica, area tao carente deatencao no Brasil.

5 Metodologia

Como esse e um projeto em uma area teorica, o metodo a ser utilizado esempre o mesmo: estudo e aprofundamento nas discussoes entre os pesquisadorese alunos envolvidos.

6 Revisao da literatura

6.1 PARTE I

6.1.1 Logica (classica) de primeira ordem

A logica classica de primeira ordem fornece uma linguagem matematica for-mal, juntamente com um sistema formal de provas, que permite uma argu-mentacao matematica correta.

Um sistema logico formal e composto de tres partes, a saber: a sintaxe(ou notacao), as regras de inferencia e a semantica (ou seja, o significado dossımbolos logicos). Partindo de um conjunto pre-definido de sımbolos (que sechama alfabeto), a notacao e dada atraves da gramatica:

F ::= A | ⊤ | ⊥ | ¬(F ) | (F ∧ F ) | (F ∨ F ) | (F ⇒ F ) | ∀x.F | ∃x.Fque significa que uma formula F pode ser atomica, verdadeira, falsa, a negacaode uma formula, a conjuncao de duas formulas, a disjuncao de das formulas,implicacao (funcao) ou formulas quantificadas (para todo e existe).

A segunda parte de um sistema logico consiste em estabelecer os axiomas eas regras de inferencia do sistema. Por exemplo, a presentacao mais difundidade logica classica possui apenas um axioma:

A ⊢ A (initial)

6

A B ¬A A ∧B A ∨B A⇒ B ⊥ ⊤V V F V V V F VV F F F V F F VF V V F V V F VF F V F F V F V

Tabela 1: Tabela da verdade

que diz que uma formula e provavel a partir de si mesma.Como exemplo de regra de inferencia, apresentamos aqui o famoso modus

ponens5:Γ ⊢ A⇒ B Γ ⊢ A

Γ ⊢ B (ELIM ⇒)

Informalmente, essa regra diz que se temos uma funcao do tipo A ⇒ B e umargumento do tipo A, entao podemos aplicar a funcao ao argumento e obter umresultado do tipo B.

Vale a pena observar que, em logica cassica, vale o tao comentado princıpiodo meio excluıdo. Ou seja, a proposicao

A ∨ ¬A

e sempre valida. Isso significa que, em matematica, uma proposicao e sempreou verdadeira, ou falsa.

Essa afirmacao e extremamente nao construtiva, uma vez que nada se podedizer de qual das das opcoes e valida.

Semantica

Com relacao a semantica, no caso proposicional (isto e, sem os quantifica-dores) o significado de formulas em logica classica e trivial, baseado na tabelada verdade. A cada sımbolo basico da logica e dado um valor (verdadeiro V oufalso F ). Dependendo desse valor, chegamos ao valor das formulas formadas apartir da gramatica analisando a Tabela 1.

Atraves dessa analise semantica, podemos ver, por exemplo, por que asformulas A⇒ B, ¬B ⇒ ¬A e ¬(A ∧ ¬B) possuem o mesmo comportamento:

A B A⇒ B ¬B ⇒ ¬A ¬(A ∧ ¬B)V V V V VV F F F FF V V V VF F V V V

Ou seja, provas matematicas do fato:

B segue de A

utilizando qualquer dos seguintes metodos:

direto, contra-positivo, por absurdo

sao equivalentes.

5Esta e uma regra de eliminacao, propria de sistemas descritos em deducao natural. Vejaa Secao 6.1.6 para a diferenca entre calculo de sequentes e deducao natural.

7

6.1.2 Logica intuicionista

Como descrito na Secao 6.1.1, o entendimento classico de logica e baseadona nocao de verdade. Ou seja, a veracidade de uma afirmativa e “absoluta” eindependente de qualquer argumentacao, crenca ou acao. Desta forma, afirma-tivas sao ou falsas ou verdadeiras (princıpio do meio excuıdo), onde falso e amesma coisa que nao verdadeiro (veja tabela da verdade acima).

Claro que essa abordagem de pensamento e muito intuitiva e baseada emexperiencia e observacao. Para um matematico preocupado em provar um teo-rema, e importante a ideia de que toda afirmativa pode ser provada - verdadeirase uma prova e apresentada ou falsa se existe um contra-exemplo. Alem disso,varias tecnicas de demostracao utilizam implicitamente o princıpio do meio ex-cluıdo.

Considere o seguinte exemplo:

Teorema 6.1 Existem dois numeros irracionais x e y tais que xy e racional.

Prova A prova desse fato e bastante simples: se 2√

2 e racional, entao toma-mos x = y =

√2.

Caso contrario, tomamos x = 2√

2 e y =√

2.Observe que nao temos como saber qual dos casos realmente acontece, porque

nao se sabe se 2√

2 e racional ou irracional. Mas o princıpio do meio excluıdonos garante que uma das opcoes ocorre e isso e bastante natural de se aceitar.Entao, para o exemplo acima descrito, o problema se limita ao fato de que aprova apresentada nao e construtiva.

Um caso mais serio surge com o seguinte teorema:

Teorema 6.2 Existem sete 7’s consecutivos na representacao decimal do numeroπ.

Ora, ou alguem algum dia chega a representacao de com um numero decasas decimais grande o suficiente de modo a encontrar sete 7’s consecutivos ouentao... nao se sabe!

Considere p a afirmativa:

existe uma prova de que existem sete 7’s consecutivos na representacaodecimal do numero π.

e chamemos de t o predicado dado pelo enunciado do Teorema 6.2. Parece claroque p ⇔ t. Mas isso vale somente se p e verdadeiro. Se p e falso nao se podedizer que t e falso.

Esse e um exemplo de uma afirmativa para a qual nao existe sentido a suanegacao. Ou seja, o princıpio do meio excluıdo nao se encaixa em um sistemaque possui esse tipo de “teorema”. Observe que aqui “infinitude” esta envolvida.Ou seja, muito provavelmente, provar o Teorema 6.2 significa testar todas as(infinitas) possibilidades.

A logica intuicionista abandona a ideia de verdade absoluta, e afirmativassao consideradas validas se e somente se existe uma prova construtiva da mesma.Ou seja, o princıpio do meio excluıdo nao e mais valido.

Semantica

8

Um dos modelos semanticos mais populares para a logica intuicionista ebaseado em algebras de Heyting. Descreveremos aqui (de maneira resumida) asemantica para o caso proposicional [37].

Seja Φ o conjunto de todas as formulas proposicionais da logica intuicionista,considere Γ ⊆ Φ e seja ∼ a seguinte relacao de equivalencia:

ϕ ∼ ψ se e somente se Γ ⊢ ϕ⇒ ψ e Γ ⊢ ψ ⇒ ϕ

Seja LΓ = Φ/ ∼= {[ϕ]∼ : ϕ ∈ Φ} e defina uma ordem parcial ≤ sobre LΓ daseguinte forma:

[ϕ]∼ ≤ [ψ]∼ se e somente se Γ ⊢ ϕ⇒ ψ.

Podemos tambem definir as seguintes (bem definidas) operacoes sobre LΓ:

[α]∼ ∪ [β]∼ = [α ∨ β]∼;

[α]∼ ∩ [β]∼ = [α ∧ β]∼;

−[α]∼ = [¬α]∼;

ou ainda ir mais adiante e mostrar que as operacoes ∩ e ∪ sao operacoes “ınfimo”e “supremo” com relacao a ≤, e que as leis de distributividade

(a ∪ b) ∩ c = (a ∩ c) ∪ (b ∩ c) e (a ∩ b) ∪ c = (a ∪ c) ∩ (b ∪ c)

sao satisfeitas6. A classe [⊥]∼ e o menor elemento (0) de LΓ e [⊤]∼, onde⊤ = ⊥ ⇒ ⊥, e o maior elemento (1). Temos tambem que [⊤]∼ = {ϕ : Γ ⊢ϕ}. Entretanto, existem algumas dificuldades (ja esperadas) com a operacaocomplementar:

−a ∩ a = [⊥]∼ mas nao necessariamente − a ∪ a = [⊤]∼.

O maximo que podemos afirmar e que −a e o maior elemento tal que −a∩a =0. Chamamos −a de pseudo-complemento de a. Uma vez que a negacao e umcaso especial de implicacao (pois ¬a ≡ a ⇒ ⊥), o que foi dito acima mereceuma generalizacao. Um elemento c e chamado um pseudo-complemento relativode a com relacao a b se e somente se c e o maior elemento tal que a ∩ c ≤ b. Opseudo-complemento relativo, caso existir, e denotado por a ⇀ b.

Nao e difıcil de ver que na algebra LΓ (comumente chamada de algebra deLindenbaum), temos

[ϕ]∼ ⇀ [ψ]∼ = [ϕ⇒ ψ]∼.

Formalmente, uma algebra de Heyting (ou algebra pseudo-Booleana), e umsistema algebrico H que e um reticulado distributivo contendo o zero e quepossui um pseudo-complemento relativo definido para cada par de elementos.Em particular, cada algebra de Boole e uma algebra de Heyting com a ⇀ bdefinido como −a ∪ b7.

A semantica da logica intuicionista proposicional e dada pela aplicacao [[•]],definida a seguir.

6Ou seja, LΓ e um reticulado distributivo.7O exemplo mais conhecido de algebra de Heyting que nao e uma algebra de Boole e a

algebra de conjuntos abertos de um espaco topologico.

9

Definicao 6.3 Seja H = 〈H,∪,∩,⇀,−, 0, 1〉 uma algebra de Heyting. Denota-mos por PV ao conjunto de variaveis proposicionais da logica intuicionista.

i. Uma valuacao v em H e uma aplicacao v : PV −→ H.

ii. Dada uma valuacao v em H, definimos a aplicacao [[•]]v : Φ −→ H por:

[[p]]v = v(p) para p ∈ PV[[⊥]]v = 0[[ϕ ∨ ψ]]v = [[ϕ]]v ∪ [[ψ]]v[[ϕ ∧ ψ]]v = [[ϕ]]v ∩ [[ψ]]v[[ϕ⇒ ψ]]v = [[ϕ]]v ⇀ [[ψ]]v

Escreveremos Γ |= ϕ sempre que [[Γ]]v = 1 implica [[ϕ]]v = 1 para todos H ev relacionados com a algebra de Heyting H.

O seguinte teorema diz que o modelo semantico baseado em algebra de Hey-ting e completo e “sound”:

Teorema 6.4 As seguintes condicoes sao equivalentes:

1. Γ ⊢ ϕ;

2. Γ |= ϕ.

6.1.3 Logica Linear

Como visto na Secao 6.1.1, matematicos comecam de um conjunto de axio-mas, provam alguns lemas e entao os utilizam para provar teoremas. Algumasdas provas utilizadas nao sao construtivas, e o uso da estrategia conhecida comoreducao ao absurdo e muito comum.

Uma vez que um lema e provado, ele pode ser usado de novo para provaroutras proposicoes ou teoremas, uma vez que um lema provado verdadeiro seraverdadeiro para sempre. Portanto, matematicos trabalham com a logica classica,a logica da verdade estavel e de recursos e conclusoes infinitos.

Ja a logica intuicionista (Secao 6.1.2) joga fora essa nocao de verdade abso-luta e a veracidade de uma afirmativa depende da existencia de uma prova (ouconstrucao) da afirmativa.

Mas ainda, a logica intuicionista e uma logica de infinitos recursos – masnao infinitas conclusoes, uma vez que permitir a prova de todos os resultadospossıveis implica em permitir o princıpio do meio excluıdo.

Agora, se imaginarmos a situacao real de descrever uma maquina de venderrefrigerantes, nao e adequado usar uma logica de recursos infinitos. Ou seja, seuma latinha de guarana custa um real e tenho um real na minha carteira, possocomprar apenas uma latinha e, no fim do processo, vou estar sem dinheiro.

A Logica Linear (desenvolvida por Girard [9]) lida com situacoes como essa:e uma logica de recursos conscientes. Em Logica Linear, afirmativas nao podemser livremente copiadas (Contraction) ou descartadas (Weakening), apenas emsituacoes especiais, onde aparece um tipo muito particular de conectivos: os ex-ponenciais “?” e “!”. Intuitivamente, !B significa que o recursoB pode ser usadotantas vezes quanto necessarias. De maneira dual, ?B indica a possibilidade deproducao de uma quantidade infinita da conclusao B.

10

A implicacao linear e representada pelo sımbolo “−◦” e o significado de A−◦Be:

consome-se A dando origem a B

Isto significa que, a partir do ponto em que B e produzido, o predicado A deixade ser valido. A implicacao intuicionista “⇒” entao significa:

A⇒ B ≡ !A−◦B

ou seja, um predicado A implica B intuicionisticamente se e somente se existeuma quantidade infinita de A que linearmente implica B.

A ausencia de Contraction e Weakening muda a natureza dos conectivoslogicos. De fato, a conjuncao intuicionista (assim como a disjuncao) e separadaem dois conectivos diferentes. Portanto, existem duas maneiras distintas deformular a conjuncao, correspondendo a dois conectivos distintos em LogicaLinear: o conectivo multiplicativo “⊗” (A⊗B significa ambos A e B) e o aditivo“&” (A&B = escolha entre A e B). O mesmo para a disjuncao: multiplicativo“O” (AOB e igual a A paralelo a B) e aditivo “⊕” (A⊕B significa ou A ou B).

Logica Linear utiliza ainda os seguintes conectivos: ⊥, e 1 para a versaomultiplicativa de falso e verdadeiro respectivamente; 0, ⊤ para a versao aditivadesses conectivos; e ∀ e ∃ para quantificacoes universal e existencial.

Semantica

A semantica da Logica Linear e dada atraves de espacos coerentes.

Definicao 6.5 Um espaco coerente e um conjunto (de conjuntos) A que satisfazas seguintes propriedades:

i. Se a ∈ A e a′ ⊂ a entao a′ ∈ A.

ii. Se M ⊂ A e se ∀a1, a2 ∈M.a1 ∪ a2 ∈ A, entao⋃M ∈ A.

Podemos entao considerar que espacos coerentes sao domınios (parcialmenteordenados pela inclusao) algebricos (qualquer conjunto e a uniao direta de seussubconjuntos finitos).

Na verdade, espacos coerentes sao uma extensao dos domınios de Scott (vejaSecao 6.2.1). Tais domınios sao caracterizados pela continuidade, onde somasdiretas sao preservadas. No caso de Logica Linear, um novo tipo de teoria dedomınios e introduzida, que possui (e preserva) pullbacks. Esta propriedadetambem e chamada de estabilidade.

Entender como espacos coerentes podem ser utilizados para descrever semanticademanda um certo tempo e muito espaco. Portanto, nao podera ser descrito nes-tas notas. Uma analise mais detalhada sobre este assunto pode ser encontradaem [9, 10].

6.1.4 Logica e Matematica

Para muitos, logica nao faz parte da matematica. De fato, parece parado-xal dizer que a logica e um ramo da matematica, uma vez que a logica e oinstrumento utilizado para o estudo da matematica.

Na realidade, o estudo da logica como um modelo para a matematica, sendoao mesmo tempo uma parte da matematica nao forma um cırculo vicioso, mas

11

pode ser entendido como uma escada em espiral. Se a matematica esta no n-esimo degrau (chamado degrau intuitivo), o degrau n + 1 contem um modeloreduzido, um prototipo (degrau formal). A passagem do degrau n para o degraun+ 1 e chamado formalizacao.

Com relacao a logica, a passagem do degrau n para o degrau n+ 1 implicaem aumentar a ordem. Entao, a logica classica de primeira ordem (que e umramo da matematica) da origem a logica de segunda ordem (que contem toda amatematica), onde predicados podem ser quantificados, e nao apenas variaveis.

Acho interessante tambem ressaltar que, nas areas classicas da matematica,o proposito inicial e propor um modelo matematico para alguma situacao maisou menos concreta. Com a logica, acontece algo similar. A sua particularidadereside no fato de que a “realidade” que a logica visa descrever nao e fora domundo matematico, mas sim a propria matematica. Desta forma, do mesmomodo que um matematico nao confunde o ambiente fısico em que vive com umespaco vetorial euclideano tri-dimensional, um pesquisador na area de logicanao a confunde com a matematica sendo descrita.

Por fim, observe que tanto na matematica quanto na logica, o estudo de mo-delos da origem ao aparecimento de novos ramos de estudo, que aparentementenada ou pouco tem a ver com o objetivo inicial de descrever um “objeto”, seja eleconcreto ou nao. Desta forma, a logica como disciplina passa a ter vida propria,e o seu estudo nao se limita ao caso classico. Isto justifica o aparecimento eestudo de logicas como a intuicionista, linear, fuzzy, modal, etc.

6.1.5 Logica e Ciencia da Computacao

De Acordo com Miller [18], logica e utilizada na especificacao de siste-mas computacionais de dois modos. Primeiro, computacoes sao estruturasmatematicas contendo nodos, estados e transicoes de estados e a logica fazafirmacoes sobre tais estruturas. Portanto, computacoes sao modelos para ex-pressoes logicas. Esta abordagem e conhecida como computacao-como-modelo.Como um exemplo de como a logica e utilizada nesta abordagem, considere astriplas de Hoare que tipicamente sao representados como:

{Γ}P{∆}

significando que se um programa P comeca a ser rodado em um estado quesatizfaz as proposicoes logicas em Γ, entao P termina (se termina) em um estadoque satisfaz as proposicoes em ∆. As formulas em Γ sao chamadas de pre-condicoes de P enquanto que as em ∆ sao chamadas de pos-condicoes. Porexemplo, seja P o programa que contem o comando x := x+1. O fato de que Pcomeca em um estado, por exemplo, em que o identificador x tem valor 1 podeser representado como o par 〈x, 1〉, dentro de uma estrutura matematica maior.A logica e utilizada para expressar proposicoes sobre este par. Por exemplo,ao final de um passo de execucao, teremos 〈x, 2〉 satizfazendo a proposicao x >1 ∧ x < 3.

Na segunda abordagem, estados sao descritos atraves de um conjunto de pro-posicoes e mudancas nos estados sao modelados por mudancas nas proposicoesdentro de uma derivacao (ou seja, por passos na construcao de uma prova). Essaabordagem e conhecida como computacao-como-deducao.

No exemplo anterior, o fato de que o identificador x tem valor 1 pode sercodificado como a proposicao “x tem valor 1”. Note que a mudanca de estado

12

pode requerer que uma certa proposicao deixe de ser valida, enquanto que outraspodem passar a ser verdadeiras. Tais mudancas sao naturalmente suportadaspela Logica Linear. De fato, a transicao do estado 1 para o estado 2 pode serdescrita como a seguinte formula da Logica Linear:

(x tem valor 1) −◦ (x tem valor 2)

Ou seja, a primeira proposicao e “consumida” para “produzir” a segunda pro-posicao.

As logicas classica e intuicionista nao suportam esse tipo de acao: um con-texto pode apenas ser expandido ao longo de uma derivacao e nao existe oconceito de limitacao ou consumo de recursos.

A primeira abordagem tem sido amplamente estudada e faz uso de topicosda matematica como teoria de conjuntos, teoria das categorias, algebras, etc,para modelar computacoes. Em geral, as estruturas matematicas utilizadas saocomplexas porque devem lidar com o conceito de infinitude.

A segunda abordagem, apesar de lidar com estruturas mais simples (queraramente fazem referencia ao infinito) e de estar mais intimamente ligada acomputacao, tem merecido pouca ou nenhuma atencao nos ultimos tempos.Apenas apos recentes pesquisas na area de teoria de provas e programacao logicaobservou-se um crescimento do estudo nessa area de pesquisa. Logicas expressi-vas como Logica Linear [9] (e Forum [17] - linguagem de programacao baseadaem Logica Linear) passaram a ser utilizadas para modelar estados, transicoesde estado e algumas primitivas de concorrencia. Como sera visto no decorrerdo texto, a utilizacao de Logica Linear para especificar sistemas computacionaisprove ricas formas de analise e deducao de propriedades dos sistemas especifi-cados.

Mais recentemente, uma nova abordagem para representar logicas foi pro-posta: o Calculo de Estruturas [6, 12, 39]. Ate agora, varias logicas proposici-onais foram especificadas em calculo de estruturas e a alta simetria das regraslogicas juntamente com o procedimento de deep inference para acessar subfor-mulas permitem a observacao de algumas propriedades muito interessantes naslogicas especificadas. Isto abre uma avenida enorme para a exploracao do usoda logica em proof theory.

6.1.6 Deducao natural versus calculo de sequentes

Na Secao 6.1.1, vimos alguns exemplos de um formalismo de provas chamadodeducao natural. A principal vantagem desse tipo de presentacao de sistemasde logica formal e que deducao natural segue o estilo natural de argumentacao,com regras de introducao e eliminacao para cada conectivo.

Entretanto, construir provas utilizando deducao natural e muito difıcil, umavez que nao existe, comecando da formula que se deseja provar e seguindo debaixo para cima, uma estrategia de prova.

Outro formalismo, chamado calculo de sequentes, e tambem muito utilizadopara presentacao de sistemas de logica formal. Calculo de sequentes foi intro-duzido nos anos 1930 por Gerhard Genzen8.

Apesar da sintaxe ser parecida, calculo de sequentes e deducao natural di-ferem em varios aspectos. Enquanto deducao natural enfatiza as propriedades

8Que, por sinal, foi quem introduziu tambem a deducao natural.

13

mais fundamentais dos conectivos atraves de suas regras de eliminacao e in-troducao, o calculo de sequentes e mais “pratico” no sentido que:

• em vez de regras de eliminacao e introducao, o calculo de sequentes possuiapenas regras de introducao;

• premissas e conclusoes sao tratadas da mesma forma e sao construıdassimultaneamente;

• e menos natural, mas tecnicamente mais simples: quando lidas de baixopra cima (bottom up), fica claro que as regras no calculo de sequentessimplificam o processo de construcao de provas.

As regras do calculo de sequentes para a logica classica estao listadas naFigura 1.

Axioma inicial e a regra cut

Γ, A ⊢ ∆, AInicial

Γ1 ⊢ ∆1, A A,Γ2 ⊢ ∆2

Γ1,Γ2 ⊢ ∆1,∆2

Cut

Regras a direita

Γ ⊢ ⊤,∆ ⊤RΓ ⊢ A,∆ Γ ⊢ B,∆

Γ ⊢ A ∧B,∆ ∧ RΓ, A ⊢ B,∆

Γ ⊢ A⇒ B,∆⇒ R

Γ ⊢ A,∆Γ ⊢ A ∨B,∆ ∨ R1

Γ ⊢ B,∆Γ ⊢ A ∨B,∆ ∨R2

Γ ⊢ A[x/y],∆

Γ ⊢ ∀xA,∆ ∀R Γ ⊢ A[x/t],∆

Γ ⊢ ∃xA,∆ ∃R

Regras a esquerda

Γ,⊥ ⊢ ∆⊥L

Γ, A ⊢ ∆

Γ, A ∧B ⊢ ∆∧ L1

Γ, B ⊢ ∆

Γ, A ∧B ⊢ ∆∧ L2

Γ, A ⊢ ∆ Γ, B ⊢ ∆

Γ, A ∨B ⊢ ∆∨ L

Γ1 ⊢ A,∆1 Γ2, B ⊢ ∆2

Γ1,Γ2, A⇒ B ⊢ ∆1,∆2

⇒ L

Γ, A[x/t] ⊢ ∆

Γ, ∀xA ⊢ ∆∀L Γ, A[x/y] ⊢ ∆

Γ, ∃xA ⊢ ∆∃L

Regras estruturais

Γ ⊢ ∆

Γ, A ⊢ ∆weak L

Γ ⊢ ∆

Γ ⊢ ∆, Aweak R

Γ, A,A ⊢ ∆

Γ, A ⊢ ∆cont L

Γ ⊢ ∆, A,A

Γ ⊢ ∆, Acont R

Figura 1: Calculo de sequentes para a logica classica

14

6.1.7 Cut elimination

Talvez a regra logica mais conhecida em deducao natural seja a modus po-nens9:

Γ ⊢ A⇒ B Γ ⊢ AΓ ⊢ B (ELIM ⇒)

Informalmente, essa regra diz que se temos uma funcao do tipo A ⇒ B e umargumento do tipo A, entao podemos aplicar a funcao ao argumento e obter umresultado do tipo B.

A regra acima citada juntamente com a regra de introducao de ⇒ e equi-valente a regra Cut do calculo de sequentes que aparece em logicas tradicionaiscomo classica, intuicionista e linear [3]:

Γ1 ⊢ ∆1, A A,Γ2 ⊢ ∆2

Γ1,Γ2 ⊢ ∆1,∆2

(Cut)

Basicamente, essa regra formaliza o conceito de provas matematicas utilizandolemas auxiliares. Ou seja, se podemos provar um lema A (e outros resultados∆1) a partir de um conjunto de hipoteses Γ1 e, a partir de A (e possivelmentealgumas outras hipoteses Γ2) e possıvel provar outro conjunto de resultados(∆2), entao podemos provar ∆1,∆2 diretamente a partir de Γ1,Γ2.

Essa ideia e utilizada sempre em Matematica mas e tambem muito interes-sante sob o ponto de vista computacional, uma vez que a implementacao detal regra e feita “bottom-up”. Ou seja, para tentar provar ∆1,∆2 a partir deΓ1,Γ2, primeiro tentamos provar uma formula A (para uma certa formula des-conhecida A), e a partir de A tentamos provar ∆2. Isto significa que a formulalogica A deve ser “adivinhada” pelo programa de computador e isso representaum problema muito serio, uma vez que computadores nao tem a “criatividade”necessaria para adivinhar formulas.

Portanto, e muito importante dentro da area de programacao logica a pos-sibilidade de se verificar se um sistema logico possui a propriedade de cut-elimination, ou seja, checar se a regra Cut e, de fato, redundante e portantopode ser eliminada.

Enquanto para Ciencia da Computacao a importancia da propriedade decut-elimination esta relacionada com a viabilidade de implementacoes, para osmatematicos essa propriedade reforca o fato de que lemas sao ferramentas uteispara organizar uma prova, mas completamente dispensaveis.

Checar se um sistema logico possui a propriedade de cut-elimination e, emgeral, um problema nao trivial (veja, por exemplo, [36, 16, 27, 19, 3]).

6.1.8 Logical frameworks

Um logical framework [26, 27] e uma meta-linguagem formal especificamentedesenvolvida para representar linguagens de programacao, logicas e outros for-malismos que podem ser descritos atraves de sistemas de provas. Um logicalframework consiste de uma meta-linguagem de representacao (usualmente umalogica ou uma teoria de tipos) com algumas propriedades computacionais, e umametodologia de meta-representacao que sugere como codificar um dado sistemade provas.

9Veja Secao 6.1.1

15

Acontece que a codificacao tem que ser natural e eficiente, se nao se tormaintratavel e inutil.

Isto significa que a meta-linguagem escolhida deve ser poderosa o suficientepara codificar diversos sistemas dedutivos e, ao mesmo tempo, deve ser simpleso suficiente de maneira a permitir representacoes concisas dos sistemas especi-ficados.

Em artigos recentes [19, 20, 5], Logica Linear tem sido usada como umframework para a especificacao de sistemas de provas. As codificacoes propostassao naturais, elegantes e diretas, permitindo o uso da rica meta-teoria da LogicaLinear para ajudar a provar propriedades sobre os sistemas especificados.

6.1.9 Logica Linear como framework para especificar sistemas desequentes

No passado, varios frameworks logicos baseados em logica intuicionista temsido propostos e utilizados para especificar sistemas de provas baseados emdeducao natural (veja por exemplo Isabelle [24], λ-Prolog [15], LF [25] e Twelf [28]).Dada a coneccao entre deducao natural e λ-calculus (veja Secao 6.2.4), aplicacoesque requerem object-level binding e substituicoes tem sido implementadas comsucesso nesses frameworks logicos.

Como exemplo, considere a prova em deducao natural:

(A)...B CD

Tal prova pode ser especificada em logica intuicionista como:

(prove A⇒ prove B) ∧ prove C ⇒ prove D

Proof search em logica intuicionista tem sido bem estudada e possui diversasimplementacoes robustas (como Isabelle e λ-Prolog acima citadas, por exemplo).

A questao que surge e: qual framework e adequado para especificar calculo desequentes? Claramente, sequentes podem ser codificados dentro dos frameworksexistentes atraves de pares de listas de formulas. Mas calculo de sequentes possuivarias dualidades:

Esquerda DireitaPositivo Negativo

Axioma inicial Regra CutSıncrono Assıncrono

Em particular, a dualidade Esquerda - Direita e o centro do calculo desequentes uma vez que sequentes tem a forma:

Γ ⊢ ∆

onde as hipoteses Γ estao do lado esquerdo do sımbolo de validade ⊢ enquantoas conclusoes ∆ ocorrem do lado direito. Relacionado a isto, esta a nocao deocorrencias positivas e negativas de uma formula dentro de um sequente. Anocao de conectivos sıncronos e assıncronos depende das regras de inferencia

16

definindo o comportamento de tais conectivos, e a dualidade do axioma inicial eda regra Cut pode ser melhor entendida dentro do topico Calculo de Estruturas(veja Secao 7).

Um framework deve levar em conta tais dualidades diretamente, e isso eproblematico em logica intuicionista. De fato, uma vez que o princıpio do meioexcluıdo nao e mais valido, temos que, em geral,

¬(¬A) 6≡ A

ou seja, negando um predicado duas vezes nao nos da o predicado original. Istofaz com que a logica intuicionista seja muito fraca como meta-logica para des-crever sistemas de sequentes uma vez que, por definicao, dualidades sao sempresimetricas.

Tambem, as regras estruturais tem um papel importante na definicao deconectivos logicos em calculo de sequentes, e um controle total da modalidadenao esta presente em logica intuicionista.

Ocorre que Logica Linear e uma boa escolha de meta-linguagem: possui umanegacao involutiva permite que Contraction e Weakening sejam controlados erefina a logica intuicionista.

6.2 PARTE II

6.2.1 λ-calculus e computabilidade

O λ-calculus [2, 33] e um sistema formal que lida com a teoria de funcoes. Foiintroduzido nos anos 1930 por Alonzo Church. Originalmente, Church tentouconstruir um sistema (que continha o λ-calculus) para a fundamentacao da ma-tematica. Mas esse sistema foi mostrado inconsistente por ser possıvel simularo paradoxo de Russell dentro da teoria10. Desta foma, Church separou a partedo λ-calculus e a usou para estudar a computabilidade.

λ-calculus e uma teoria que representa funcoes como regras, ao inves datradicional abordagem de funcoes como graficos. Funcoes como regras e a nocaomais antiga de funcao11 e refere-se ao processo de partir de um argumento paraum valor, processo esse determinado apenas por uma definicao e por certasregras.

Desta forma, e possıvel estudar os apectos computacionais das funcoes. Porexemplo, podemos pensar em funcoes determinadas por definicoes em portuguesaplicadas a argumentos tambem expressos em portugues. Ou, mais especifica-mente, funcoes dadas como programas aplicadas a outros programas. Em ambosos casos, temos uma estrutura livre de tipos, onde os objetos de estudo sao, aomesmo tempo, funcao e argumento.

Esse e o ponto de partida para o λ-calculus atipado. Em particular, umafuncao pode ser aplicada a ela mesma. Na nocao usual de funcao em matematica(como na teoria de conjuntos de Zermelo-Fraenkel), isso e impossıvel (por causado “axioma de fundacao”).

De maneira formal, termos em λ-calculus sao definidos da seguinte forma.

10De fato, o paradoxo de Russell pode ser representado atraves do λ-termo:(λx.not (xx))(λx.not (xx)) onde not (xx) e verdadeiro se x nao e um elemento de x.

11Essa ideia de funcoes como regras surgiu antes mesmo da ideia, usualmente atribuıda aDirichlet, de que funcoes podem ser consideradas como graficos, i.e., como conjuntos de pares:(argumento, valor).

17

Definicao 6.6 Seja V ar um conjunto enumeravel finito de variaveis. O con-junto Λ de λ-termos e definido pela seguinte gramatica:

M ::= x | λx.M | MM

ou seja, um λ-termo pode ser uma variavel (x ∈ V ar), uma abstracao ou umaaplicacao de termos.

Observe que um λ-termo e uma funcao com apenas um argumento que, porsua vez, vem a ser uma funcao com um unico argumento, etc. Dessa forma, setem uma ideia intuitiva do porque λ-calculus trata de funcoes recursivamenteenumeraveis.

Funcoes sao definidas atraves de uma λ-expressao que expressa a acao dafuncao em seu argumento. Por exemplo, a funcao

f(x) = x+ 2

e expressa em λ-calculus comoλx.x + 2

que significa que o comportamento da funcao e de adicionar 2 ao argumento,caso exista. Observe que o nome da funcao (antes f) nao importa, ou seja, foiabstraıda. Tambem nao importa se a funcao e ou nao aplicada a um argumento(no caso de f , o argumento era x), uma vez que isso nao e necessario paradescrever o comportamento da funcao. Mais do que isso, a λ-funcao pode seraplicada a um numero natural, real, ou a uma outra funcao, o que nao e possıvelcom a representacao usual de funcoes.

O λ-calculus possui apenas uma regra de reducao, que basicamente diz queaplicar uma funcao a um argumento significa substituir todas as ocorrencias davariavel da funcao pelo argumento em questao.

Definicao 6.7 i) A regra β e definida como:

(λx.M)N →M [N/x]

ii) A β-reducao e o fechamento contextual da regra β, representada por →β.

Entao, considerando o exemplo de funcao definido acima,

(λx.x + 2)5 →β (x + 2)[5/x] = 5 + 2 = 7

Essa reducao corresponde, no caso usual, ao calculo do valor da funcao f parax = 5:

f(5) = 5 + 2 = 7

O λ-calculus pode ser considerado a menor linguagem de programacao uni-versal. Menor no sentido que possui uma unica regra de reducao (a reducaoβ, que nada mais e que a substituicao de variaveis). Universal porque todasas funcoes computaveis podem ser expressas utilizando esse formalismo (tese deChurch).

Apesar de ser possıvel programar em λ-calculus, a sua real importanciapara Ciencia da Computacao e que muitos problemas de design de linguagense de implementacao, especialmente aqueles que dizem respeito a estrutura de

18

tipos, sao mais faceis de serem investigados dentro do λ-calculus do que emlinguagens de programacao mais complexas. Por isso dizemos que o λ-calculuse um instrumento teorico utilizado para provar propriedades sobre aplicacoespraticas.

O λ-calculus com a β-reducao definida acima da origem a uma estrategiade passagem de parametros chamada call-by-name, onde os parametros naoprecisam ser avaliados antes de serem fornecidos a funcao. Essa estrategia eutilizada em linguagens de programacao como ML, por exemplo.

Existem termos em λ-calculus para os quais se pode construir sequenciasinfinitas de reducoes. O exemplo classico e:

(λx.xx)(λx.xx) →β (λx.xx)(λx.xx) →β . . .

Tais termos sao utilizados para modelar o comportamento de sub-rotinas queentram em loop, por exemplo.

Mas os λ-termos mais importantes de estudo sao aqueles que, para qualquerestrategia de reducao escolhida, a reducao sempre para. Tais termos sao chama-dos fortemente normalizaveis. Um resultado importante aparece em [32], ondee apresentada uma caracterizacao sintatica do conjunto de termos fortementenormalizaveis atraves de um sistema de intersection types (veja Secao 6.2.3).

Apesar de ser uma caracterizacao interessante, o sistema apresentado porPottinger nao apresenta tanta importancia pratica porque as regras do sistemasao por vezes muito difıcieis de serem manipuladas. Portanto, uma caracte-rizacao sintatica usando conjuntos, como e um dos objetivos deste projeto, e degrande interesse.

Outra nocao importante ligada a reducao β e a de lazy evaluation.

Definicao 6.8 A β-reducao lazy e o fechamento aplicativo da regra β, repre-sentada por →βl.

Em outras palavras, uma reducao e dita lazy se o corpo da funcao e avaliadoapenas quando um argumento e fornecido. Em λ-calculus, esse tipo de avaliacaoe modelado por uma estrategia de reducao que nao reduz β-redexes que ocorremdentro do escopo de uma λ-abstracao.

O λ-calculus com a β-reducao lazy definida acima da origem a uma estrategiade passagem de parametros chamada call-by-value, onde os parametros devemser avaliados antes de serem fornecidos a funcao. Essa estrategia e utilizada emlinguagens de programacao como Haskell, por exemplo.

A nocao de normalizacao forte pode ser estendida para o caso lazy de umamaneira bem natural: um termo e fortemente lazy normalizavel se e somente seo termo possui uma forma normal lazy e nao existe uma sequencia infinita dereducoes lazy partindo dele.

No trabalho [22] foi apresentada uma caracterizacao sintatica para o con-junto de termos de λ-calculus que sao fortemente lazy normalizaveis. O obje-tivo (d) deste projeto e fazer o mesmo para termos fortemente normalizaveis12.Desta forma, darıamos uma caracterizacao completa de termos fortemente nor-malizaveis tanto no call-by-name quanto no call-by-value λ-calculus.

12Observe que todo termo fortemente normalizavel e fortemente lazy normalizavel mas ocontrario nao e verdadeiro. De fato, o termo λx.((λx.xx)(λx.xx)) e fortemente lazy norma-lizavel mas nao fortemente normalizavel. Outra observacao interessante e que a forma normallazy, quando existe, pode nao ser unica.

19

Semantica

Finalmente, algumas consideracoes sobre semantica. A semantica do λ-calculus pode ser dada atraves de categorias cartesianas fechadas ou aindaatraves de Domınios de Scott. Um Domınio de Scott e um CPO (conjuntoparcialmente ordenado) algebrico, limitado e completo. Na verdade, a unica di-ferenca entre um Domınio de Scott e um reticulado e que o primeiro nao precisater necessariamente um elemento maximo.

A dificuldade em se estabelecer a semantica do λ-calculus reside no fato deque funcoes tomam funcoes como argumento e assim sucessivamente, permitindoa existencia de operadores de ponto fixo Y . Estes, por definicao, possuem apropriedade M(YM) = YM para todos os termos M do λ-calculus.

Durante anos, para formular uma semantica denotacional para o λ-calculus,tentou-se construir um modelo no qual funcoes (totais) eram associadas a cadaλ-termo. Tal modelo formalizaria um elo entre o λ-calculus como um sistemasintatico puro e o λ-calculus como um sistema notacional para manipular funcoesmatematicas concretas. Infelizmente, tal modelo nao pode existir pois, se hou-vesse uma funcao associada ao operador Y , esta teria que computar o ponto fixode funcoes arbitrarias, e existem funcoes (a funcao sucessor, por exemplo) quenao possuem ponto fixo. Logo, uma funcao correspondente a Y deve ser umafuncao parcial, necessariamente nao definida para alguns argumentos.

Dana Scott superou esta dificuldade atraves da formalizacao da nocao deinformacao parcial ou incompleta para representar computacoes que nunca ter-minam. Em adicao, o domınio de computacao e equipado com uma relacao deordem parcial, onde o “resultado indefinido” e o menor elemento.

O passo importante para encontrar um modelo para o λ-calculus foi consi-derar apenas as funcoes que possuem um ponto fixo. Desta forma, o domınioobtido contem o seu espaco de funcoes (X ≃ X → X), e portanto funcoespodem ser aplicadas a elas mesmas!

Por fim, vale a pena ressaltar que que domınios tambem permitem umainterpretacao intuitiva. A ordem parcial de um domınio representa a hierarquiade informacao ou conhecimento. Quanto “maior” o elemento, mais especıficoele e, e maior quantidade de informacao ele contem. Elementos “menores”representam conhecimento incompleto ou resultados intermediarios.

Computacao e entao modelada pela iteracao de funcoes monotonas, primei-ramente aplicadas ao menor elemento. Chegar a um ponto fixo (na verdade, omenor deles) equivale a terminar a computacao.

6.2.2 λ-calculus tipado simples

Tipos estao presentes tanto em matematica quanto em computacao. Nateoria de conjuntos tradicional, o agrupamento de elementos em um conjuntoindepende da natureza desses elementos.

Quando passamos a trabalhar em aplicacoes especıficas, precisamos classifi-car os objetos em categorias, de acordo com o seu uso ou aplicacao. A nocao detipos origina-se dessa classificacao: um tipo e uma colecao de objetos ou valoresque possuem alguma propriedade em comum.

Em matematica, tipos impoem restricoes que evitam paradoxos. Universosnao tipados, como o da teoria de conjuntos de Frege, apresentam inconsistenciaslogicas (tais como o paradoxo de Russell).

20

Tipos τ ::= b tipo basico (ou primitivo)τ1 → τ2 tipo funcional

Termos e ::= x variavelλ x : τ. e λ-abstracaoe e′ aplicacao

Figura 2: Sintaxe livre de contexto do λ-calculus tipado simples

Em computacao, existem diversas linguagens nao tipadas, por exemplo:LISP, λ-calculus, Self, Perl e Tcl. Essas linguagens nao dispoem de nenhummecanismo para a deteccao de falhas devidas a operacoes aplicadas a argumen-tos improprios. O estudo de tipos em linguagens de programacao tornou-se degrande importancia, especialmente por causa de sua influencia sobre o projeto ea definicao de linguagens de programacao e, portanto, sobre o desenvolvimentode software em geral.

A definicao de uma linguagem de programacao deve especificar tanto a sin-taxe quanto a semantica da linguagem. A sintaxe determina quais sequenciasde sımbolos sao frases (validas), e como frases podem ser combinadas de modoa formar outras frases.

O uso de um formalismo baseado em logica (constituıdo por axiomas e regrasde inferencia) possibilita definir a sintaxe de linguagens de programacao. A ideiadesses sistemas formais e estabelecer regras de formacao das frases da lingua-gem, a partir de suas subfrases, levando em conta propriedades das construcoesenvolvidas na formacao dessas frases.

Tais propriedades consideradas sao tipos de expressoes e os sistemas resultan-tes sao denominados sistemas de tipos. Para o caso do λ-calculus simplesmentetipado, a sintaxe das expressoes e apresentada na Figura 2.

Ja o axioma e as regras de inferencia de tipos para o λ-calculus simplesmentetipado sao apresentados na Figura 3.

Γ, x : τ ⊢ x : τ(V AR)

Γ ⊢ e : τΓ, x : τ ′ ⊢ e : τ

(ADV AR)

Γ, x : τ ′ ⊢ e : τ

Γ ⊢ (λx : τ ′. e) : τ ′ → τ(ABS)

Γ ⊢ e : τ ′ → τ, Γ ⊢ e′ : τ ′

Γ ⊢ e e′ : τ(APL)

Figura 3: Sistema de tipos do λ-calculus tipado simples

As principais propriedades do λ-calculus tipado simples sao: confluencia enormalizacao (herdadas do λ-calculus nao tipado); expressoes nao podem ser

21

Tipos τ ::= b tipo basico (ou primitivo)τ1 → τ2 tipo funcionalτ1 ∩ τ2 tipo intersecao

Figura 4: Tipo intersecao

aplicadas a si proprias; nao se pode definir o operador de ponto fixo na proprialinguagem; propriedade de terminacao (normalizacao forte): toda sequencia dereducao de qualquer expressao termina, ou seja, toda expressao possui uma(unica) forma normal.

Entretanto, nem toda expressao fortemente normalizavel pode ser tipada noλ-calculus tipado simples. O exemplo classico e o termo λx.xx, que esta ja emforma normal, mas contem uma auto-aplicacao, nao tipavel em λ-calculus tipadosimples. Tal termo pode ser tipado, entretanto, no sistema de tipos intersecao(IT ), que apresentaremos a seguir.

6.2.3 Sistema de tipos intersecao

A sintaxe de termos do sistema de tipos intersecao e a mesma do λ-calculustipado simples. Com relacao aos tipos, acrescenta-se o tipo intersecao (Figura 4).

O axioma e as regras de inferencia de tipos para o sistema de tipos intersecaosao os mesmos do λ-calculus simplesmente tipado (V AR, ADDV AR, ABS,APPL) mais as regras para o conectivo intersecao apresentadas na Figura 5.

Γ ⊢ e : τ1 ∩ τ2Γ ⊢ e : τ1

(ELIMR)

Γ ⊢ e : τ1 ∩ τ2Γ ⊢ e : τ2

(ELIML)

Γ ⊢ e : τ1 Γ ⊢ e : τ2Γ ⊢ e : τ1 ∩ τ2

(INTI)

Figura 5: Sistema de tipos do intersection types

Desta forma, o termo λx.xx possui tipo ((α → β) ∩ α) → β no sistema detipos intersecao. De uma maneira geral [32]:

Teorema 6.9 Um termo M do λ-calculus e fortemente normalizavel se e so-mente se existem um contexto Γ e um tipo intersecao τ tal que Γ ⊢M : τ .

O problema de tal caracterizacao e que ela envolve provas em um sistema detipos. E o problema com esse sistema de tipos e que a regra (INTI), quandoanalisada de cima pra baixo – que e como um procedimento de prova logica seda – impoe que o termo e seja o mesmo para ambas as premissas. Isso tornao sistema indecidıvel e, portanto, praticamente intratavel. Uma caracterizacaopor conjuntos seria bem mais importante na pratica.

22

A motivacao original do estudo de IT foi a de propor novos λ-modelos bemcomo analizar propriedades de normalizacao, como descrito acima. Mas valeressaltar que, nos ultimos 20 anos, o escopo da pesquisa em IT tem se alargado.Van Bakel [42] escreveu um bom sumario das pesquisas realizadas ate meadosda decada de 1990, e Wells [44] cita outros avancos importantes e mais recentesdo uso de IT em Ciencia da Computacao.

6.2.4 Isomorfismo de Curry-Howard

O isomorfismo de Curry-Howard estabelece uma correspondencia muito inte-ressante entre sistemas de logica formal (tratados em teoria de provas) e calculoscomputacionais (como aqueles em teoria de tipos).

A relacao no caso de logica intuicionista em deducao natural e λ-calculus(tipado simples) estebelece que:

• formulas correspondem a tipos;

• provas correspondem a termos;

• provabilidade corresponde a reducao de termos.

Desta forma, os dois mundos que sao objeto de estudo no presente projeto –logica e teoria de funcoes – que, a princıpio, parecem ser de mundos diferentes,estao intrinsecamente ligados. Tal isomorfismo entre o λ-calculus simplesmentetipado e a logica intuicionista foi estabelecida por volta de 1940.

Outro caso interessante de estudo e quando o calculo e baseado em inter-section types. Desde a sua criacao, em 1980, pergunta-se se existe uma logicacorrespondente ao calculo de tipos intersecao. Tal logica foi apresentada apenasem 2004 no trabalho [30] e e baseada na nocao de sincronismo de processos.

Mais especificamente, em [30] foi apresentado uma justificativa proof theo-retical para o sistema de tipos intersecao atraves da apresentacao do sistemalogico ISL (para Intersection Synchronous Logic). ISL e um sistema de classesde equivalencia de deducoes do fragmento implicativo e conjuntivo da logicaintuicionista.

Tal resultado e altamente teorico, e importante no sentido que:

1. resolve um problema em aberto desde 1980;

2. estabelece de uma vez por todas a diferenca entre a conjuncao e a in-tersecao;

3. prove um metodo imediato para provar a normalizacao forte dos tiposintersecao, fato ja conhecido, mas para qual o metodo de prova e extre-mamente complicado.

O que parece ser tambem uma consequencia (e esta sim seria de cunhopratico), e que se pode propor uma linguagem de programacao que suportepolimorfismo discreto, com a garantia de que toda computacao para.

23

7 Principais contribuicoes cientıficas

7.1 PARTE I

Em [20], varios sistemas logicos foram especificados utilizando Logica Linearcomo meta-logica. As codificacoes foram feitas de uma maneira muito direta enatural, e isso permitiu a utilizacao da rica meta-teoria da Logica Linear paraprovar propriedades interessantes sobre as logicas-objeto.

Sendo a Logica Linear uma linguagem de programacao abstrata (no sentidode Miller [17]), todos os sistemas especificados puderam ser implementados ealgumas propriedades cujas provas nao requerem inducao foram verificadas demaneira automatica.

Dentre essas propriedades, podemos citar: um modo simples de descrevermodularmente a distincao entre as logicas classica e intuicionista; como os mo-dais de Logica Linear colapsam quando aplicados a atomos nessas duas logicas;como codificar sistemas que fazem um uso mais refinado dos modais (como o taofalado sistema LU [11]); provas de cut-elimination parcialmente automatizadas.

Em [19], Logica Linear foi utilizada para provar a propriedade de cut-eliminationpara todos os sistemas previamente especificados em [20]. Tal prova e aindasemi-automatizada, uma vez que a automacao total exigiria uma meta-logicacom inducao sobre provas.

O objetivo (a) deste projeto e encontrar uma estrategia para a automacaocompleta de algumas provas (tais como cut-elimination), utilizando Logica Li-near com inducao (natural, estrutural e sobre provas) e definicao.

Alguns resultados preliminares podem ser encontrados no artigo [29], ondee apresentado um logical framework chamado Llinda, onde ja aparece a ideia deLogica Linear com definicao e inducao.

Com relacao ao objetivo (c), o resultado pretendido e inedito e visa prover ummetodo para analisar a estrutura de provas. Observando que certas definicoessao positivas e outras negativas (dependendo dos conectivos utilizados no corpodos predicados definidos), podemos provar propriedades sobre os predicados edeterminar a estrutura de uma prova utilizando a nocao de polaridades. Essafoi uma das muitas ideias que surgiram durante a minha estadia no INRIA emdezembro de 2005, trabalhando com o Prof. Dale Miller.

So para dar uma ideia de como usar polaridade em Logica Linear, se con-siderarmos as formulas a e b como positivas, entao a prova polarizada de ⊢a⊥ ⊗ b, aOb⊥ seria:

⊢ a ⇓ a⊥(Initial)

⊢ b ⇓ b⊥(Initial)

⊢ b⊥, b ⇓(⇓)

⊢ b⊥, b ⇑(⇑)

⊢ b⊥ ⇑ b(⇑)

⊢ b⊥ ⇓ b(⇑)

⊢ a, b⊥ ⇓ a⊥ ⊗ b(⊗R)

⊢ a⊥ ⊗ b, a, b⊥ ⇑(⇓)

⊢⇑ a⊥ ⊗ b, a, b⊥(⇑)

⊢⇑ a⊥ ⊗ b, aOb⊥(OR)

24

Se a e b forem negativas, entao a prova seria simetrica:

⊢ a ⇓ a⊥(Initial)

⊢ a⊥, a ⇓(⇓)

⊢ a⊥, a ⇑(⇑)

⊢ a⊥ ⇑ a(⇑)

⊢ a⊥ ⇓ a(⇑)

⊢ b ⇓ b⊥(Initial)

⊢ a, b⊥ ⇓ a⊥ ⊗ b(⊗R)

⊢ a⊥ ⊗ b, a, b⊥ ⇑(⇓)

⊢⇑ a⊥ ⊗ b, a, b⊥(⇑)

⊢⇑ a⊥ ⊗ b, aOb⊥(OR)

O exemplo acima e simples no sentido que o unico fato observado e que re-verter a polaridade de formulas reverte a prova das mesmas. Mas se a e b saoatomos definidos de maneira recursiva 13, entao a inversao de polaridades deter-mina a mudanca de estategia de provas matematicas. E isso e bem interessante,tanto matematicamente quanto computacionalmente.

O objetivo (b) deste projeto se refere ao Calculo de Estruturas. O Calculode Estruturas (CoS) ([3, 4, 12, 38, 39, 40]) e um novo formalismo teorico, in-troduzido pelo Prof. Alessio Guglielmi em 1999 e desenvolvido principalmentepelo Grupo de Inteligencia Artificial em Dresden.

CoS explora a simetria (observada a partir do surgimento do conceito dedeep inference [6, 7]), tornando possıvel estender a dualidade natural entre re-gras de inferencia de um dado conectivo para uma extraordinaria dualidade emderivacoes. Esta simetria permite a reducao da regra Cut para a sua versaoatomica, atraves de um procedimento completamente diferente daqueles utili-zados em provas tradicionais de cut-elimination.

Este resultado e extremamente interessante e merece maior atencao. E umdos objetivos deste projeto e exatamente tentar juntar tudo o que tem sido feitoutilizando os dois formalismos: Logica Linear (calculo de sequentes) e Calculo deEstruturas. De fato, resultados preliminares mostram que e possıvel representarsistemas dedutivos no Calculo de Estruturas e analisar suas propriedades, comofazemos em calculo de sequentes, deducao natural e proof nets.

O principal proposito deste novo formalismo (CoS) e permitir uma analisemais rica em provas que outros formalismos permitem. Isto e baseado em duasideias principais: inferencias sao simetricas com relacao a premissas e conclusoes,e elas sao aplicaveis dentro de expressoes logicas (formulas), o que se chama deepinference. Como consequencia, e conveniente fazer deducoes sobre estruturas,que sao expressoes intermediarias entre formulas e sequentes.

Na presenca de uma negacao involutiva, o Calculo de Estruturas generaliza,de maneira trivial, o calculo de sequentes, ao mesmo tempo que permite maisliberdade no design de sistemas dedutivos. Desta maneira, e possıvel proporsistemas onde todas as regras sao atomicas, ou locais, incluindo a regra Cut.

A teoria de provas do Calculo de Estruturas difere significativamente daqueleestudado ate agora. Deep inference muda consideravelmente os metodos usuaisde cut-elimination, mas ao mesmo tempo possui a bencao de ser restrita aformulas atomicas.

13como os numeros naturais: nat x△

= [x = z] ⊕ ∃y.[x = suc y ⊗ nat y]

25

Finalmente, os sistemas dedutivos no Calculo de Estruturas sao simples eelegantes, e portanto o Calculo de Estruturas parece ser o candidato perfeitopara a especificacao de sistemas logicos.

Alguns resultados importantes ja foram obtidos durante a realizacao do mes-trado do aluno Mario Sergio Alvim e os resultados serao submetidos para apre-sentacao em uma conferencia internacional e futura publicacao em revista in-ternacional indexada.

7.2 PARTE II

Uma parte do meu trabalho de pesquisa atual consiste em estudar logica,tipos intersecao e os λ-termos fortemente normalisaveis, ou seja, aqueles para osquais toda β-reducao termina, independente da estrategia de reducao adotada.Em termos matematicos, eu estudo, utilizando metodos baseados em logica, oconjunto das funcoes que podem ser definidas de maneira recursivamente enu-meravel e que sempre retornam um resultado quando submetidas a computacao.

E sabido que a pertinencia de uma funcao nesse conjunto e indecidıvel. Entaouma caracterizacao sintatica a partir de conjuntos construıdos de maneira re-cursiva e mais simplese mais facil de ser implementada.

Em [22], foi apresentada uma caracterizacao sintatica completa da classe determos fortemente lazy normalizaveis utilizando um sistema logico e um sistemade tipos intersecao adequado.

Essa caracterizacao, alem de ser interessante por si mesma, permite umaconexao importante entre o λ-calculus call-by-name e call-by-value.

O objetivo de (d) e retirar a palavra lazy de tudo que foi dito no paragrafoanterior, apresentando uma descricao sintatica completa do conjunto de termosfortemente normalizaveis. Desta forma, pretende-se estender o resultado obtidoem [32] de modo a tornar o entendimento e o “manuseio” de tal conjunto maistratavel. Vale ressaltar que, ao que tudo indica, esta e a melhor carecterizacaosintatica possıvel, ou seja, e o melhor que pode ser feito nessa direcao.

Com relacao ao segundo objetivo do projeto, (e) e a continuacao do que foifeito em [30] (e descrito na Secao anterior), uma vez que o estudo que temosdesenvolvido ate agora levam a crer que se pode propor uma linguagem deprogramacao que suporte polimorfismo discreto.

Na verdade, uma versao preliminar desta parte do projeto ja esta pronta efoi apresentada no Structures and Deduction, workshop associado ao ICALP(julho, 2005).

O trabalho descrito na PARTE II sera realizado em colaboracao com osprofessores Simona Ronchi della Rocca, Luca Paolini e Luca Roversi, todosdo Departamento de Informatica da Universidade de Turim, Italia. Espera-sea publicacao de 2 artigos em revista internacional indexada e um artigo emproceedings de congresso internacional.

8 Identificacao dos demais participantes do pro-

jeto

Pesquisadores:

26

• Dale Miller – Diretor de Pesquisa INRIA-FUTURS (Paris - Franca); pro-fessor da Ecole Polytechnique. Foi meu orientador de doutorado e e meuatual colaborador.

• Simona Ronchi della Rocca – Full Professor da Universita degli Studi diTorino, (Italia). Trabalhei com ela durante o meu pos doutorado.

• Luca Paolini – Pesquisador da Universita degli Studi di Torino, (Italia).Trabalhei com ele durante o meu pos doutorado.

• Luca Roversi – Professor Assistente da Universita degli Studi di Torino,(Italia). Trabalhei com ele durante o meu pos doutorado.

Aluno de doutorado:

• Mario Sergio Ferreira Alvim Junior – foi aceito para o programa de douto-rado do INRIA - FUTURS. Comeca as atividades em dezembro de 2008.

Alunos de Mestrado:

• Carlos Salvador Murray – aluno do curso de Ciencia da Computacao, 2o

ano.

• Fabiana Lopes Fernandes – aluna do curso de Matematica, 2o ano.

Alunos de graduacao:

• Giselle Machado Nogueira Reis – aluna do curso de Ciencia da Com-putacao, 8o perıodo.

• Henrique Antunes Almeida – aluno do curso de Filosofia, 4o perıodo.

• Frederico Augusto Menezes Ribeiro – aluno do curso de Matematica, 6o

perıodo.

• Joyce Figueiro – aluna do curso de Matematica Computacional, 2o perıodo.

9 Apoios, parcerias ja estabelecidas e contrapar-

tidas das instituicoes financeiras

Como foi dito anteriormente, este projeto esta inserido dentro dos seguintesprojetos europeus:

• PARSIFAL – http://www.lix.polytechnique.fr/parsifal/ coordenado peloProf. Dale Miller (INRIA - FRANCA).

• SLIMMER – http://www.lix.polytechnique.fr/Labo/Dale.Miller/slimmer/coordenado pelo Prof. Dale Miller.

• Calculus of Structures – http://www.computational-logic.org/˜guglielm/group/coordenado pelo Prof. Alessio Guglielmi (Bath)

• FOLLIA – http://follia.di.unito.it/index.html, coordenado pela Profa. Si-mona Ronchi della Rocca (UNITO).

Alem disso, uma parte deste projeto foi contemplado com 02 bolsas de Ini-ciacao Cientıfica, um laptop e uma impressora no Edital Universal de 2007 daFAPEMIG, que devera terminar no final de 2009.

27

Referencias

[1] Amtoft, T. and Turbak, F. Faithful translations between polyvari- ant owsand polymorphic types. In Programming Languages and Systems, 9th Eu-ropean Symp. Programming, LNCS vol. 1782, pp. 26–40 (2000).

[2] Barendregt, H.P., The Lambda Calculus: its syntax and semantics, N.103in Studies in Logic and the Foundations of Mathematics (revised edition),North-Holland, Amsterdam (1994).

[3] Bruscoli, P. and Guglielmi, A., A Tutorial on Proof Theoretic Foundationsof Logic Programming. Invited tutorial at ICLP ’03, LNCS 2916 (2003).

[4] Bruscoli, P. and Guglielmi, A., On Structuring Proof Search for First OrderLinear Logic, LPAR ’03, LNCS 2850, pp. 389–406 (2003).

[5] Cervesato, I. and Pfenning, F. A linear logical framework. Information &Computation, 179(1), pp. 19–75 (2002).

[6] Brunnler, K., Deep Inference and Symmetry in Classical Proofs, PhD thesis(2003).

[7] Brunnler, K., Atomic Cut Elimination for Classical Logic, CSL 2003, LNCS2803, pp. 86-97 (2003).

[8] Girard, J-Y. The System F of Variable Types: Fifteen Years Later, Theo-retical Computer Science, vol. 45, pp.159–192 (1986).

[9] Girard, J-Y., Linear Logic, Theoretical Computer Science, vol 50, pp. 1–102(1987).

[10] Girard, J-Y., Proofs and types.

[11] Girard, J-Y., On the unity of logic, Annals of Pure and Applied Logic, vol.59, pp. 201–217 (1993).

[12] Guglielmi, A. A System of Interaction and Structure, to appear on ACMTransactions on Computational Logic.

[13] Godel, K. On Undecidable Propositions of Formal Mathematical Systems,New York (1934).

[14] Hatcher, W. S. Foundations of Mathematics (1968).

[15] Nadathur, G. and Miller, G. An Overview of λ-Prolog, Fifth InternationalLogic Programming Conference (1988).

[16] McDowell, R. and Miller, D., Cut elimination for a logic with definitionsand induction, Theoretical Computer Science, vol. 232, pp.91–119 (2000).

[17] Miller, D., Forum: A multiple-conclusion specification language, Theoreti-cal Computer Science, vol.165, pp. 201–232 (1996).

[18] Miller, D. Sequent Calculus and the Specification of Computation, SchoolMarktoberdorf on Logic of Computation in 1997: An Advanced StudyInstitute of the NATO Science Committee and the Technical Universityof Munich, Germany (1997).

28

[19] Miller, D., Pimentel, E., Using linear logic to reason about sequent systems,Proceedings of Tableaux, Lecture Notes in Computer Science (2002).

[20] Miller, D., Pimentel, E., Linear logic as a framework for specifying sequentcalculus, Lectures in Logic 17 (2004).

[21] Palsberg, J. and Pavlopoulou, C. From polyvariant flow information tointersection and union types. Journal of Functional Programming, 11(3),pp. 263–317 (2001).

[22] Paolini, L., Pimentel, E., Ronchi della Rocca, S., Lazy Strong Normaliza-tion, Eletronic Notes in Theoretical Computer Science, to appear, 2004.

[23] Paolini, L., Pimentel, E., Ronchi della Rocca, S., A non lazy call-by-valueλ-calculus, submitted for publication (2006).

[24] Paulson, L., C. The Foundation of a Generic Theorem Prover, Journal ofAutomated Reasoning, vol. 5 (1989).

[25] Pfenning, F. Elf: A Language for Logic Definition and Verified Meta-programming, Fourth Annual Symposium on Logic in Computer Science(1989).

[26] Pfenning, F. Logical and meta-logical frameworks. In G. Nadathur, editor,Proceedings of the International Conference on Principles and Practice ofDeclarative Programming (1999).

[27] Pfenning, F. Logical frameworks. In Alan Robinson and Andrei Voronkov,editors, Handbook of Automated Reasoning, chapter 17, pp. 1063–1147(2001).

[28] Pfenning, F. and Schurmann, C. System description: Twelf - a meta-logicalframework for deductive systems. In H. Ganzinger, editor, Proceedings ofthe 16th International Conference on Automated Deduction (1999).

[29] Pimentel, E., Miller, D., On the specification of sequent systems, LPAR(2005).

[30] Pimentel, E., Ronchi della Rocca, S., Roversi, L., Intersection types:a proof-theoretical approach, Proceedings of Structures and Deduction,workshop associated to ICALP’05 (2005).

[31] Pimentel, E., Ronchi della Rocca, S., Roversi, L., Intersection types anddiscrete polymorphism, draft (2005).

[32] G. Pottinger, “A type assignment for the strongly normalizable λ-terms”,in To H.B. Curry: essays on combinatory logic, lambda calculus and for-malism, pp.561-577, Academic Press, London, 1980.

[33] Ronchi Della Rocca S., Paolini L., The Parametric λ-calculus: a meta-model for computation, Computer Science-Monograph, Springer Verlag,(2004).

[34] Reynolds, J. C., Towards a type theory of type structure, ProgrammingSymposium, LNCS 19, pp. 408–425 (1974).

29

[35] Russell, B. and Whitehead, A. N., Principia Mathematica, New York, Cam-bridge University Press (1927).

[36] Schroeder-Heister, P. Cut-elimination in logics with definitional reflection,Lecture Notes in Computer Science 619 (1992).

[37] Sørensen, M. H. and Urzyczyn, P. Lectures on the Curry-Howard iso-morphism (1998).

[38] Straßburger, L., MELL in the calculus of structures. Theoretical ComputerScience, vol. 309, pp. 213–285 (2003).

[39] Straßburger, L., Linear Logic and Noncommutativity in the Calculus ofStructures, Ph.D. thesis (2003).

[40] Straßburger, L., Non-commutativity and MELL in the Calculus of Structu-res, Theoretical Computer Science, vol. 309, pp. 213–285 (2003).

[41] Turing, A.M. On Computable Numbers, with an Application to the Ents-cheidungsproblem, Proceedings of the London Mathematical Society, series2, 42 pp , 230-265 (1936-37).

[42] van Bakel, S. Intersection Type Assignment Systems, Theoretical ComputerScience, 151(2), pp. 385–435 (1995).

[43] Wells, J. B., Dimock, A., Muller, R. and Turbak, F. A calculus with poly-morphic and polyvariant flow types, Journal of Functional Programming,12(3), pp. 183–227 (2002).

[44] Wells, J. B. and Haack, C. Branching types, to appear in Information andComputation.

30