Coordination scientifique : Jean-Baptiste Joinet (IRPhiL Lyon 3) et Hugo Cadière (IRPhiL Lyon 3)
 

Thématique scientifique générale du programme LICP (Résumé) :

Les récents succès très médiatisés de l’Apprentissage Machine (AM) en IA ont remis le focus sur la question de l’intelligibilité des processus computationnels. En effet, dans le cadre de ces techniques, “programmer” n’est pas combiner des instructions de programmation dotées d’une sémantique opérationnelle (forme standard pour la programmation via des langages informatiques “impératifs”), mais une sorte d’éducation (un dressage progressif), par essais et erreurs, les succès étant renforcés “de l’extérieur” (via des validations et des coefficients de pondération) et par des boucles de rétroactions.

Dans un tel paradigme, nulle conscience claire, chez le “dresseur d’IA”, de l’algorithme incorporé dans l’IA dressée (algorithme au sens où on l’entend pour une “programmation informatique” par combinaison d’instructions). L’IA dressée reste inexplicable, inintelligible : la manière dont, face à des entrées, celle-ci produit, au terme d’un processus, un résultat, est extensionnellement descriptible (les paramètres de l’IA dressée sont connus), mais le processus computationnel induit demeure essentiellement opaque, inexplicable (non interprétable comme combinaison d’instructions).

Si la question de l’Intelligibilité des processus computationnels prend un sens aigu dans le cadre récent de l’IA, cette problématique lui pré-existait dans le cadre traditionnel des langages de programmation et est même en réalité constitutive de l’apparition, autour de 1930, des premiers “langages de programmation”.

De fait, le premier d’entre eux, le lambda calcul de Church (et son noyau purement fonctionnel : le lambda calcul pur) fut introduit explicitement comme tentative de dépassement de l’inintelligibilité dévoilée par les paradoxes découverts au début du siècle dans le puissant langage logique frégéen ("mes développements [...] ne suffisent pas à assurer dans tous les cas une référence à mes combinaisons de signes", Frege, 1902, lettre à Russell). Par cette proposition (alternative à celle conçue par Russell via sa théorie des types) Church, à partir de 1934, recentre en effet la question sémantique, sur les propriétés, la structure et la “générativité” de la dynamique computationnelle induite par ce langage (réalisée par la conversion locale d'un texte en un autre texte, en fonction du co-texte).

Les premières réflexions de Church sur les conditions rendant potentiellement le processus computationnel source de dénotation et d’intelligibilité se concentrent ainsi sur des propriétés comme la potentielle non terminaison de la dynamique computationelle, mais aussi la potentielle non-terminaison en fonction des “chemins” computationnels (“stratégies” d’exécution). C’est dans le prolongement de ces travaux germinaux qu’émergera vers 1960 la toujours actuelle “Sémantique des programmes” au sens large (et notamment la “Sémantique dénotationnelle” introduite par Ch. Strachey et D.Scott). Les investigations dans ce champ, pris au sens large, visent différents niveaux d’intelligibilité des processus computationnels “purs” (i.e. non typés, cf. plus loin) : à identifier des invariants de la computation, à distinguer des comportements algorithmes spécifiques (construction de l'individu algorithmique, distinction du comportement individuel, saisi à un niveau possiblement variable, plus ou moins fin, d'intensionalité), à anticiper (analyse statique) certaines propriétés de la dynamique computationnelle de programmes particuliers (terminaison, complexité, distinctions intensionnelles…).

Le projet visé propose une enquête centrée sur la sémantique de la computation, à la fois sur les racines de ce questionnement (à l’intersection de la logique et de la pensée philosophique autour du calcul et du calculable), mais aussi sur son actualité dans l’informatique théorique contemporaine (du calcul parallèle aux modèles concurrents, du calcul quantique à l’apprentissage machine).
 

Programme du colloque

(en anglais)
 

MONDAY 13/10, afternoon

SESSION 1: Semantics and constructivity

14:30-15:30 Victor BARROSO-NASCIMENTO (University College London) - Higher-order Kripke models for intuitionistic and non-classical modal logics

Abstract

Title: Higher-order Kripke models for intuitionistic and non-classical modal logics
 
Abstract: This talk discusses a new proposal of semantics for intuitionistic and non-classical modal logics obtained through higher-order Kripke models, a new generalization of standard Kripke models that is remarkably close to Kripke's original idea - both mathematically and conceptually. Standard Kripke models are now considered 0-ary models, whereas an n-ary model for n > 0 is a model whose set of objects (''possible worlds'') contains only (n-1)-ary Kripke models. This framework is obtained by promoting a radical change of perspective in how modal semantics for non-classical logics are defined: just like classical modalities are obtained through use of an accessibility relation between classical propositional models, non-classical modalities are now obtained through use of an accessibility relation between non-classical propositional models (even when they are Kripke models already). This talk is mostly dedicated to discussing how such semantics can be provided for some intuitionistic modal logics and what are the main conceptual and technical novelties of the new framework, but it will also cover how the semantics for one such modal logic (called MK) naturally leads to a generalization that works for non-classical modal logics in general. It will be shown that, depending on which intuitionistic 0-ary propositional models are allowed, we may obtain 1-ary models equivalent to birelational models for logics such as IK or MK. Those 1-ary models have an intuitive reading that adds to the interpretation of intuitionistic propositional models in terms of ''timelines'' the concept of ''alternative timelines''. More generally, any n-ary model can be read as defining a concept of ''alternative'' for any substantive interpretation of its (n-1)-ary models. The semantic clauses for necessity and possibility of MK are then shown to be modular and thus usable if one wishes to obtain similar modal semantics for any other non-classical logic, each of which can be provided with a similar intuitive reading. Higher-order Kripke models can thus be considered a promising new semantics for non-classical modal logics in general, as witnessed by the results already obtained for intuitionistic modal logics in particular.

15:45-16:45 Joaquim T. WADDINGTON (University College London) - Base-extension semantics for Prawitz's ecumenical system

Abstract

Title: Base-extension Semantics for Prawitz’s ecumenical system
 
Abstract: The objective of this talk is to present a Base-extension semantics for the propositional fragment of the ecumenical system N E proposed by Prawitz in 2015.
Ecumenical systems are systems in which different logics coexist peacefully. The system N E is an ecumenical system for classical and intuitionistic logic. It includes three types of logical connectives: neutral connectives (conjunction and negation), classical connectives (classical disjunction and classical implication), and intuitionistic connectives (intuitionistic disjunction and intuitionistic implication).

Proof-theoretic semantics (PtS) is a semantic theory that grounds the validity of inferences in the notion of proof as opposed to the notion of truth. In model theory, the meaning of logical connectives is given by their truth conditions. In contrast, PtS seeks to explain the meaning of logical connectives through conditions of assertability.

Base-extension semantics (BeS) is a branch of PtS where the notion of proof is defined for an atomic base (a collection of sentences free of logical connectives) and inductively extended to non-atomic formulas through semantic clauses. First, the notion of proof is defined for an atomic base; then, logical validity is defined as provability in all bases.

In 2015, Sandqvist developed a Base-extension semantics for intuitionistic logic. In this talk, I will present a way to adapt Sandqvist’s semantic clauses to obtain a semantics for the ecumenical system N E_p. The main modifications are: (I) the addition of a clause for classical implication and one for classical disjunction, and (II) treating ⊥ as part of the atomic base rather than a logical connective.

17:00-18:00 Luiz Carlos PEREIRA (Universidade Estadual do Rio de Janeiro) - On Prawitz' unpublished proof of the constructive validity of classical principles
 

TUESDAY 14/10, morning
SESSION 2: Philosophy of computation

09:00-10:00 Alberto NAIBO (IHPST, Université Paris 1 Panthéon-Sorbonne) - The epistemic features of algorithms
10:15-11:15 Mariana ANTONUTTI (IHPST, Université Paris 1 Panthéon-Sorbonne) - About Robin Gandy’s philosophy of mathematics and his conception of the mechanization of mathematical thought
11:30-12:30 Paolo PISTONE  (Université Lyon 1 &  LIP-Plume ENS de Lyon) - On Knowledge Through and Knowledge About Algorithms
 

TUESDAY 14/10, afternoon
SESSION 3: Logic and expressivity

14:00-15:00 Marcelo E. CONIGLIO (Instituto de Filosofia e Ciências Humanas & Centro de Lógica, Epistemologia e História da Ciência, Universidade Estadual de Campinas – UNICAMP) - Hyperalgebraic structures induced by hyperlattices: Applications to non-classical logics
15:15-16:15 Bruno LOPES (Universidade Federal Fluminense, UFF) - A note on Propositional Dynamic Logic expressiveness and complexity