Valentin D. Richard

Valentin D. Richard

In structural proof theory, designing and working on large calculi make it difficult to get intuitions about each rule individually and as part of a whole system. We introduce two novel tools to help working on calculi using the approach of graph theory and automata theory. The first tool is a Proof Tree Automaton (PTA): a tree automaton which language is the derivation language of a calculus. The second tool is a graphical representation of a calculus called Proof Tree Graph (PTG). In this directed hypergraph, vertices are sets of terms (e.g. sequents) and hyperarcs are rules. We explore properties of PTA and PTGs and how they relate to each other. We show that we can decompose a PTA as a partial map from a calculus to a traditional tree automaton. We formulate that statement in the theory of refinement systems. Finally, we compare our framework to proof nets and string diagrams.

Yoan Géran, Bastien Laboureix, Corto Mascle et al.

We introduce a new formalisation of languages, called keyboards. We consider a set of elementary operations (writing/erasing a letter, going to the right or to the left,...) and we define a keyboard as a set of finite sequences of such operations, called keys. The corresponding language is the set of words obtained by applying some sequence of those keys. Unlike classical models of computation, every key can be applied anytime. We define various classes of languages based on different sets of elementary operations, and compare their expressive powers. We also compare them to well-known classes of languages (Chomsky hierarchy). We obtain a strict hierarchy of languages, whose expressivity is orthogonal to the one of the aforementionned classical models. -- Nous introduisons une nouvelle représentation de langages, les claviers. On se munit d'un ensemble d'opérations élémentaires (ajout, effacement d'une lettre, déplacement à droite, à gauche, ...), et on définit un clavier comme un ensemble de suites finies d'opérations élémentaires, appelées touches. Son langage sera l'ensemble des mots obtenus en appliquant une suite quelconque de touches. Contrairement à des modèles de calcul classiques, toutes les touches peuvent être appliquées à tout moment. En premier lieu nous définissons différentes classes de claviers en faisant varier l'ensemble des opérations élémentaires autorisées, et nous comparons l'expressivité des classes de langages obtenues. Nous comparons également ces classes à la hiérarchie de Chomsky. Nous obtenons que toutes les classes étudiées sont différentes, et nous caractérisons les classes inclues dans les rationnels et les algébriques. L'expressivité des claviers semble orthogonale à celle des modèles évoqués précédemment.

Valentin D. Richard

Feature Structures (FSs) are a widespread tool used for decompositional frameworks of Attribute-Value associations. Even though they thrive in simple systems, they lack a way of representing higher-order entities and relations. This is however needed in Frame Semantics, where semantic dependencies should be able to connect groups of individuals and their properties, especially to model quantification. To answer this issue, this master report introduces wrappings as a way to envelop a sub-FS and treat it as a node. Following the work of [Kallmeyer, Osswald 2013], we extend its syntax, semantics and some properties (translation to FOL, subsumption, unification). We can then expand the proposed pipeline. Lexical minimal model sets are generated from formulas. They unify by FS value equations obtained by LTAG parsing to an underspecified sentence representation. The syntactic approach of quantifiers allows us to use existing methods to produce any possible reading. Finally, we give a transcription to type-logical formulas to interact with the context in the view of dynamic semantics. Supported by ideas of Frame Types, this system provides a workable and tractable tool for higher-order relations with FS.

Valentin D. Richard

Lambek Grammars (LG) are a computational modelling of natural language, based on non-commutative compositional types. It has been widely studied, especially for languages where the syntax plays a major role (like English). The goal of this internship report is to demonstrate that every Lambek Grammar can be, not entirely but efficiently, expressed in Abstract Categorial Grammars (ACG). The latter is a novel modelling based on higher-order signature homomorphisms (using $λ$-calculus), aiming at uniting the currently used models. The main idea is to transform the type rewriting system of LGs into that of Context-Free Grammars (CFG) by erasing introduction and elimination rules and generating enough axioms so that the cut rule suffices. This iterative approach preserves the derivations and enables us to stop the possible infinite generative process at any step. Although the underlying algorithm was not fully implemented, this proof provides another argument in favour of the relevance of ACGs in Natural Language Processing.