Linéarité : un outil analytique pour l'étude de la complexité et de la sémantique des langages de programmation, Linearity : an analytic tool in the study of complexity and semantics of programming languages

Marco Gaboardi

Description

Sous la direction de Jean-Yves Marion, Simona Ronchi Della Rocca
Thèse soutenue le 12 décembre 2007: Université de Torino - ITALIE, INPL
Dans la première partie, on propose un système de type pour le lambda-calcul, dans le style du calcul des séquents, nomme « Soft Type Assignment » (STA) qui est inspiré par la logique linéaire « soft ». STA a la propriété de réduction du sujet et est correct et complète pour les calculs en temps polynomial. Par la suite on propose un déduction naturelle, STA_N. Ce système est simple mais il a le désavantage que les variables dans le sujet peuvent être explicitement renommées. Pour résoudre ce problème, on propose le système STA_M, où les contextes sont des multi-ensembles, donc les règles pour renommer les variables peuvent être interdit. L’inférence de type pour STA_M ne semble pas décidable. On propose un algorithme qui pour chaque lambda-terme rend l’ensemble de contraintes que doivent être satisfait pour que le terme soit type. Pi est correct et complet. Ensuite on étend le lambda-calcul par des constantes booléennes et on propose le système STA_B. La particularité de STA_B est que la règle du conditionnel utilise les contextes de façon additive. Chaque programme de STA_B peut être exécuté, par une machine abstraite, en espace polynomial. De plus le système est aussi complet pour PSPACE. Dans la deuxième partie, on propose une restriction de PCF, nommée SlPCF. Ce langage est équipé avec une sémantique opérationnelle qui mélange l’appelle par nom et l’appelle par valeur et peut être interprèté en mode standard dans les espaces cohérents linéaires. SlPCF est complet pour les fonctions récursives, mais il n’est pas complet et donc il n’est pas fully abstract pour les espaces cohérents linéaires
-Complexité implicite
-Logique linéaire
-Lambda-calcul
-Sémantique denotationelle
In the first part, we propose, inspired by Soft Linear Logic, a type assignment system for lambda-calculus in sequent calculus style, named Soft Type Assignment (STA). STA enjoys the subject reduction property. and is correct and complete for polynomial time computations. Then, we propose a natural deduction named STA_N. While simple, STA_N has the disadvantage of allowing the explicit renaming of variables in the subject. To overcome to this problem, we propose another natural deduction system, named STA_M, where contexts are multisets, hence rules renaming variables can be avoided. The type inference for STA_M seems in general undecidable. We propose an algorithm Pi returning, for every lambda-term, a set of constraints that need to be satisfied in order to type the term. Pi is correct and complete. We extend the lambda-calculus by basic boolean constants and we propose the system STA_B. The peculiarity of STA_B is that the conditional rule treats the contexts in an additive way. Every STA_B program can be executed, through an abstract machine, in polynomial space. Moreover, STA_B is also complete for PSPACE. In the second part we propose a restriction of PCF, named SlPCF. The language is naturally equipped with an operational semantics mixing call-by-name and call-by-value parameter passing and it can be interpreted in linear coherence space in a standard way. SlPCF is recursive complete, but it is not complete, and thus not fully abstract, with respect to linear coherence spaces
-Implicit computational complexity
-Denotational semantics
-Linear logic
-Lambda-calculus
Source: http://www.theses.fr/2007INPL099N/document

Sujets

• Logique linéaire
• Lambda-calcul

Informations

• Publié par: Thesee
• Nombre de lectures: 40
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

AVERTISSEMENT



Ce document est le fruit d’un long travail approuvé par le jury de
soutenance et mis à disposition de l’ensemble de la communauté
universitaire élargie.
Il est soumis à la propriété intellectuelle de l’auteur au même titre que sa
version papier. Ceci implique une obligation de citation et de
référencement lors de l’utilisation de ce document.
D’autre part, toute contrefaçon, plagiat, reproduction illicite entraîne une
poursuite pénale.

Contact SCD INPL : [e-mail]




LIENS




Code de la propriété intellectuelle. Articles L 122.4
Code de la propriété intellectuelle. Articles L 335.2 – L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm
Dipartimento di Informatica
Università degli Studi di Torino
Ecole doctorale IAEM Lorraine
Institut National Polytechnique de Lorraine
Linearity: an Analytic Tool in the Study of
Complexity and Semantics of Programming Languages
THÈSE
présentée et soutenue publiquement le 12 decembre 2007
pour l’obtention du
Doctorat de l’Institut National Polytechnique de Lorraine
(spécialité informatique)
et du
Doctorat de l’Universitá degli studi di Torino
(spécialité informatique)
par
Marco Gaboardi
Composition du jury
Rapporteurs: Jacqueline Vauzeilles Professeur, Université Paris XIII
Simone Martini Professeur, Universitá di Bologna
Examinateurs: Patrick Baillot Chargé de Recherche, CNRS
Paolo Coppola Professeur, Universitá di Udine
Jean-Yves Marion Professeur, ENSMN-INPL
Simone Martini Professeur, Universitá di Bologna
Simona Ronchi Della Rocca Professeur, Universitá di Torino
Jacqueline Vauzeilles Professeur, Université Paris XIIIDipartimento di Informatica
Università degli Studi di Torino
Ecole doctorale IAEM Lorraine
Institut National Polytechnique de Lorraine
Dottorato di Ricerca in Informatica
Ciclo XX
Linearity: an Analytic Tool in the Study of
Complexity and Semantics of Programming Languages
Marco Gaboardi
Supervisori:
Prof.ssa Simona Ronchi Della Rocca
Prof. Jean-Yves Marion
Coordinatore del dottorato:
Prof. Pietro Torasso
Anni Accademici: 2004-2005 2005-2006 2006-2007
Settore scientifico-disciplinare di afferenza: INF/01Acknowledgments
First and foremost, I express my gratitude to my first supervisor Simona Ronchi Della
Rocca. Her invaluable guidance has taught me a lot. Her great enthusiasm and con-
creteness in doing research have been source of inspiration in my work. Without her
help and patience this thesis would not have been possible.
I owe a great debt to my second supervisor Jean-Yves Marion for his support during my
staying in Nancy. His suggestions on the directions of my works have been important.
Without his guidance a good part of this thesis would never have been written.
I would express my thanks to Jacqueline Vauzeilles and Simone Martini for accepting
to be the referees of this thesis and for their valuable comments. I would thank Patrick
Baillot and Paolo Coppola for being part of my phd committee. I owe my gratitude to
PatrickBaillotalsoformanyhelpfulcommentsandsuggestionsonthisthesis. Moreover,
he has made it possible my staying in Paris. I enjoyed very much this period spent in
interesting and stimulating discussions.
I am in debt with Luca Roversi. His interest in Implicit Computational Complexity and
the many stimulating discussions on different topics have greatly influenced me.
IexpressmythankstoLucaPaoliniforhavingsharedwithmehisideasthathaveleaded
to the second part of this thesis.
I am grateful to Felice Cardone, my former supervisor, who has brought me to Torino
and has always patiently listened and helped me.
I would thank many colleagues for stimulating conversations. In particular, Luca Fos-
sati and the other phd students, Mauro Piccolo and the other members of the Lambda
group, Ugo Dal Lago, Paolo Di Giamberardino, Michele Pagani, Romain Péchoux, Colin
Riba, Matthieu Kaczmarek, Virgile Mogbil, Damiano Mazza, Gabriele Pulcini.
I would also thank the friends that have made pleasant my staying in Nancy. My par-
ticular thanks goes to Noelia, Patrick, Romain, Clémence, Matthieu, Sophie, Julien,
Guillem, Heinrich, Colin, Hana, Lucia, Uwe, Clara.
My gratitude goes also to all the people who are a constant presence in my every day
life. In particular, I am extremely grateful to my family. They are a constant source
of backing and help. Finally, my special thanks goes to Anne. She has shared with me
these three years, giving me her invaluable understanding and support.
iST
A
N
PCF
ST
ST
ST
A
ST
ST
`
A
ST
ST
M
A
A
N
ST
ST
`
A
PCF
N
A
ST
A
A
A
M
A
ST
A
A
M
M
ST
ST
A
A
A
ST
ST
A
ST
Résume : Dans la première partie, on propose un système de type pour le lambda-
calcul, dans le style du calcul des séquents, nomme " Soft Type Assignment " ( )
qui est inspiré par la logique linéaire " soft ". a la propriété de réduction du
sujet et est correct et complète pour les calculs en temps polynomial. Par la suite on
propose un déduction naturelle, . Ce système est simple mais il a le désavantage
que les variables dans le sujet peuvent être explicitement renommées. Pour résoudre
ce problème, on propose le système , où les contextes sont des multi-ensembles,
donc les règles pour renommer les variables peuvent être interdit. L’inférence de type
pour ne semble pas décidable. On propose un algorithme Π qui pour chaque
lambda-terme rend l’ensemble de contraintes que doivent être satisfait pour que le
terme soit type. Π est correct et complet. Ensuite on étend le lambda-calcul par des
constantes booléennes et on propose le système . La particularité de estB B
que la règle du conditionnel utilise les contextes de façon additive. Chaque programme
de peut être exécuté, par une machine abstraite, en espace polynomial. DeB
plus le système est aussi complet pour PSPACE. Dans la deuxième partie, on propose
une restriction de PCF, nommée S . Ce langage est équipé avec une sémantique
opérationnelle qui mélange l’appelle par nom et l’appelle par valeur et peut être
interprèté en mode standard dans les espaces cohérents linéaires. S est complet
pour les fonctions récursives, mais il n’est pas complet et donc il n’est pas fully abstract
pour les espaces cohérents linéaires.
Mot clés : complexité implicite, lambda-calcul, logique linéaire, sémantique denota-
tionelle.
Abstract: In the first part, we propose, inspired by Soft Linear Logic, a type
assignment system for lambda-calculus in sequent calculus style, named Soft Type
Assignment ( ). enjoys the subject reduction property. and is correct and com-
plete for polynomial time computations. Then, we propose a natural deduction named
. While simple, has the disadvantage of allowing the explicit renaming
of variables in the subject. To overcome to this problem, we propose another natural
deduction system, named , where contexts are multisets, hence rules renaming
variables can be avoided. The type inference for seems in general undecidable.
We propose an algorithm Π returning, for every lambda-term, a set of constraints
that need to be satisfied in order to type the term. Π is correct and complete. We
extend the lambda-calculus by basic boolean constants and we propose the system
. The peculiarity of is that the conditional rule treats the contexts in anB B
additive way. Every program can be executed, through an abstract machine, inB
iiiA
ST
`
PCF
`
PCF
polynomial space. Moreover, is also complete for PSPACE. In the second part weB
propose a restriction of PCF, named S . The language is naturally equipped with
an operational semantics mixing call-by-name and call-by-value parameter passing and
it can be interpreted in linear coherence space in a standard way. S is recursive
complete, but it is not complete, and thus not fully abstract, with respect to linear
coherence spaces.
Key words : implicit computational complexity, lambda-calculus, linear logic, denota-
tional semantics.
iv