arXiv subjects

Christian Retoré

Publications and source records attributed to Christian Retoré.

At least 19 recordsLinked to original sources

arXiv2024

A proof-theoretical approach to some extensions of first order quantification

Generalised quantifiers, which include Henkin's branching quantifiers, have been introduced by Mostowski and Lindström and developed as a substantial topic application of logic, especially model theory, to linguistics with work by Barwise, Cooper, Keenan. In this paper, we mainly study the proof theory of some non-standard quantifiers as second order formulae . Our first example is the usual pair of first order quantifiers (for all / there exists) when individuals are viewed as individual concepts handled by second order deductive rules. Our second example is the study of a second order translation of the simplest branching quantifier: ``A member of each team and a member of each board of directors know each other", for which we propose a second order treatment.

math.LO↗

arXiv2023

Pomset logic: the other approach to non commutativity in logic

Thirty years ago, I introduced a non-commutative variant of classical linear logic, called "pomset logic", issued from a particular categorical interpretation of linear logic known as coherence spaces. In addition to the usual commutative multiplicative connectives of linear logic, pomset logic includes a non-commutative connective, "$\triangleleft$" called "before", associative and self-dual: $(A\triangleleft B)^\perp=A^\perp \triangleleft B^\perp$. The conclusion of a pomset logic proof is a Partially Ordered MultiSET of formulas. Pomset logic enjoys a proof net calculus with cut-elimination, denotational semantics, and faithfully embeds sequent calculus. The study of pomset logic has reopened with recent results on handsome proof nets, on its sequent calculus, or on its following calculi like deep inference by Guglielmi and Strassburger. Therefore, it is high time we published a thorough presentation of pomset logic, including published and unpublished material, old and new results. Pomset logic (1993) is a non-commutative variant of linear logic (1987) as for Lambek calculus (1958!) and it can also be used as a grammatical formalism. Those two calculi are quite different, but we hope that the algebraic presentation we give here, with formulas as algebraic terms and with a semantic notion of proof (net) correctness, better matches Lambek's view of what a logic should be.

cs.LO↗

arXiv2021

Flag: a Self-Dual Modality for Non-Commutative Contraction and Duplication in the Category of Coherence Spaces

After reminding what coherences spaces are and how they interpret linear logic, we define a modality "flag" in the category of coherence spaces (or hypercoherences) with two inverse linear (iso)morphisms: "duplication" from (flag A) to ((flag A) < (flag A)) and "contraction" in the opposite direction -- where < is the self dual and non-commutative connective known as "before" in pomset logic and known as "seq(ential)" in the deep inference system (S)BV. In addition, as expected, the coherence space A is a retract of its modal image (flag A). This suggests an intuitive interpretation of (flag A) as "repeatedly A" or as "A at any instant" when "before" is given a temporal interpretation. We hope the semantic construction of flag(A) will help to design proof rules for "flag" and we briefly discuss this at the end of the paper.

cs.LO↗

arXiv2020

Logical Semantics, Dialogical Argumentation, and Textual Entailment

In this chapter, we introduce a new dialogical system for first order classical logic which is close to natural language argumentation, and we prove its completeness with respect to usual classical validity. We combine our dialogical system with the Grail syntactic and semantic parser developed by the second author in order to address automated textual entailment, that is, we use it for deciding whether or not a sentence is a consequence of a short text. This work-which connects natural language semantics and argumentation with dialogical logic-can be viewed as a step towards an inferentialist view of natural language semantics.

cs.CL↗

arXiv2016

Aristotle's square of opposition in the light of Hilbert's epsilon and tau quantifiers

Aristotle considered particular quantified sentences in his study of syllogisms and in his famous square of opposition. Of course, the logical formulas in Aristotle work were not modern formulas of mathematical logic, but ordinary sentences of natural language. Nowadays natural language sentences are turned into formulas of predicate logic as defined by Frege, but, it is not clear that those Fregean sentences are faithful representations of natural language sentences. Indeed, the usual modelling of natural language quantifiers does not fully correspond to natural language syntax, as we shall see. This is the reason why Hilbert's epsilon and tau quantifiers (that go beyond usual quantifiers) have been used to model natural language quantifiers. Here we interpret Aristotle quantified sentences as formulas of Hilbert's epsilon and tau calculus. This yields to two potential squares of opposition and provided a natural condition holds, one of these two squares is actually a square of opposition i.e. satisfies the relations of contrary, contradictory, and subalternation.

math.LO↗

arXiv2016

Natural Language Semantics and Computability

This paper is a reflexion on the computability of natural language semantics. It does not contain a new model or new results in the formal semantics of natural language: it is rather a computational analysis of the logical models and algorithms currently used in natural language semantics, defined as the mapping of a statement to logical formulas - formulas, because a statement can be ambiguous. We argue that as long as possible world semantics is left out, one can compute the semantic representation(s) of a given statement, including aspects of lexical meaning. We also discuss the algorithmic complexity of this process.

cs.CL↗

arXiv2016

Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation

This report first shows the equivalence bewteen several formulations of classical logic in intuitionistic logic (tertium non datur, reductio ad absurdum, Pierce's law). Then it establishes the correctness of the Gödel-Kolmogorov translation, whose restriction to the propositional case is due to Glivenko. This translation maps a formula $F$ of first order logic to a formula $F^{\lnot\lnot}$ in such a way that $F$ is provable in classical logic if and only if $F^{\lnot\lnot}$ is provable in intuitionistic logic. All formal proofs are presented in natural deduction. These questions are well-known proof theoretical facts, but in textbooks, they are often ignored or left to the reader. Because of the combinatorial difficulty of some of the needed formal proofs, we hope that this report may be useful, in particular to students and colleagues from other areas.

math.LO↗

arXiv2014

Typed Hilbert Epsilon Operators and the Semantics of Determiner Phrases (Invited Lecture)

The semantics of determiner phrases, be they definite de- scriptions, indefinite descriptions or quantified noun phrases, is often as- sumed to be a fully solved question: common nouns are properties, and determiners are generalised quantifiers that apply to two predicates: the property corresponding to the common noun and the one corresponding to the verb phrase. We first present a criticism of this standard view. Firstly, the semantics of determiners does not follow the syntactical structure of the sentence. Secondly the standard interpretation of the indefinite article cannot ac- count for nominal sentences. Thirdly, the standard view misses the linguis- tic asymmetry between the two properties of a generalised quantifier. In the sequel, we propose a treatment of determiners and quantifiers as Hilbert terms in a richly typed system that we initially developed for lexical semantics, using a many sorted logic for semantical representations. We present this semantical framework called the Montagovian generative lexicon and show how these terms better match the syntactical structure and avoid the aforementioned problems of the standard approach. Hilbert terms rather differ from choice functions in that there is one polymorphic operator and not one operator per formula. They also open an intriguing connection between the logic for meaning assembly, the typed lambda calculus handling compositionality and the many-sorted logic for semantical representations. Furthermore epsilon terms naturally introduce type-judgements and confirm the claim that type judgment are a form of presupposition.

cs.CL↗

arXiv2014

Normalization and sub-formula property for Lambek with product and PCMLL -- Partially Commutative Multiplicative Linear Logic

This paper establishes the normalisation of natural deduction or lambda calculus formulation of Intuitionistic Non Commutative Logic --- which involves both commutative and non commutative connectives. This calculus first introduced by de Groote and as opposed to the classical version by Abrusci and Ruet admits a full entropy which allow order to be relaxed into any suborder. Our result also includes, as a special case, the normalisation of natural deduction the Lambek calculus with product, which is unsurprising but yet unproved. Regarding Intuitionistic Non Commutative Logic with full entropy does not have up to now a proof net syntax, and that for linguistic applications, sequent calculi which are only more or less equivalent to natural deduction, are not convenient because they lack the standard Curry-Howard isomorphism.

cs.LO↗

arXiv2014

Deverbal semantics and the Montagovian generative lexicon

We propose a lexical account of action nominals, in particular of deverbal nominalisations, whose meaning is related to the event expressed by their base verb. The literature about nominalisations often assumes that the semantics of the base verb completely defines the structure of action nominals. We argue that the information in the base verb is not sufficient to completely determine the semantics of action nominals. We exhibit some data from different languages, especially from Romance language, which show that nominalisations focus on some aspects of the verb semantics. The selected aspects, however, seem to be idiosyncratic and do not automatically result from the internal structure of the verb nor from its interaction with the morphological suffix. We therefore propose a partially lexicalist approach view of deverbal nouns. It is made precise and computable by using the Montagovian Generative Lexicon, a type theoretical framework introduced by Bassac, Mery and Retoré in this journal in 2010. This extension of Montague semantics with a richer type system easily incorporates lexical phenomena like the semantics of action nominals in particular deverbals, including their polysemy and (in)felicitous copredications.

cs.CL↗

arXiv2014

Category theory, logic and formal linguistics: some connections, old and new

We seize the opportunity of the publication of selected papers from the \emph{Logic, categories, semantics} workshop in the \emph{Journal of Applied Logic} to survey some current trends in logic, namely intuitionistic and linear type theories, that interweave categorical, geometrical and computational considerations. We thereafter present how these rich logical frameworks can model the way language conveys meaning.

math.CT↗

arXiv2014

A type theoretical framework for natural language semantics: the Montagovian generative lexicon

We present a framework, named the Montagovian generative lexicon, for computing the semantics of natural language sentences, expressed in many sorted higher order logic. Word meaning is depicted by lambda terms of second order lambda calculus (Girard's system F) with base types including a type for propositions and many types for sorts of a many sorted logic. This framework is able to integrate a proper treatment of lexical phenomena into a Montagovian compositional semantics, including the restriction of selection which imposes the nature of the arguments of a predicate, and the possible adaptation of a word meaning to some contexts. Among these adaptations of a word's sense to the context, ontological inclusions are handled by an extension of system F with coercive subtyping that is introduced in the present paper. The benefits of this framework for lexical pragmatics are illustrated on meaning transfers and coercions, on possible and impossible copredication over different senses, on deverbal ambiguities, and on "fictive motion". Next we show that the compositional treatment of determiners, quantifiers, plurals,... are finer grained in our framework. We then conclude with the linguistic, logical and computational perspectives opened by the Montagovian generative lexicon.

cs.LO↗

arXiv2014

Plurals: individuals and sets in a richly typed semantics

We developed a type-theoretical framework for natural lan- guage semantics that, in addition to the usual Montagovian treatment of compositional semantics, includes a treatment of some phenomena of lex- ical semantic: coercions, meaning, transfers, (in)felicitous co-predication. In this setting we see how the various readings of plurals (collective, dis- tributive, coverings,...) can be modelled.

cs.CL↗

arXiv2013

Semantic Types, Lexical Sorts and Classifiers

We propose a cognitively and linguistically motivated set of sorts for lexical semantics in a compositional setting: the classifiers in languages that do have such pronouns. These sorts are needed to include lexical considerations in a semantical analyser such as Boxer or Grail. Indeed, all proposed lexical extensions of usual Montague semantics to model restriction of selection, felicitous and infelicitous copredication require a rich and refined type system whose base types are the lexical sorts, the basis of the many-sorted logic in which semantical representations of sentences are stated. However, none of those approaches define precisely the actual base types or sorts to be used in the lexicon. In this article, we shall discuss some of the options commonly adopted by researchers in formal lexical semantics, and defend the view that classifiers in the languages which have such pronouns are an appealing solution, both linguistically and cognitively motivated.

cs.CL↗

arXiv2013

Logique mathématique et linguistique formelle

As the etymology of the word shows, logic is intimately related to language, as exemplified by the work of philosophers from Antiquity and from the Middle-Age. At the beginning of the XX century, the crisis of the foundations of mathematics invented mathematical logic and imposed logic as a language-based foundation for mathematics. How did the relations between logic and language evolved in this newly defined mathematical framework? After a survey of the history of the relation between logic and linguistics, traditionally focused on semantics, we focus on some present issues: 1) grammar as a deductive system 2) the transformation of the syntactic structure of a sentence to a logical formula representing its meaning 3) taking into account the context when interpreting words. This lecture shows that type theory provides a convenient framework both for natural language syntax and for the interpretation of any of tis level (words, sentences, discourse).

math.LO↗

arXiv2013

Learning Lambek grammars from proof frames

In addition to their limpid interface with semantics, categorial grammars enjoy another important property: learnability. This was first noticed by Buskowsky and Penn and further studied by Kanazawa, for Bar-Hillel categorial grammars. What about Lambek categorial grammars? In a previous paper we showed that product free Lambek grammars where learnable from structured sentences, the structures being incomplete natural deductions. These grammars were shown to be unlearnable from strings by Foret and Le Nir. In the present paper we show that Lambek grammars, possibly with product, are learnable from proof frames that are incomplete proof nets. After a short reminder on grammatical inference à la Gold, we provide an algorithm that learns Lambek grammars with product from proof frames and we prove its convergence. We do so for 1-valued also known as rigid Lambek grammars with product, since standard techniques can extend our result to $k$-valued grammars. Because of the correspondence between cut-free proof nets and normal natural deductions, our initial result on product free Lambek grammars can be recovered. We are sad to dedicate the present paper to Philippe Darondeau, with whom we started to study such questions in Rennes at the beginning of the millennium, and who passed away prematurely. We are glad to dedicate the present paper to Jim Lambek for his 90 birthday: he is the living proof that research is an eternal learning process.

cs.LG↗

arXiv2013

Advances in the Logical Representation of Lexical Semantics

The integration of lexical semantics and pragmatics in the analysis of the meaning of natural lan- guage has prompted changes to the global framework derived from Montague. In those works, the original lexicon, in which words were assigned an atomic type of a single-sorted logic, has been re- placed by a set of many-facetted lexical items that can compose their meaning with salient contextual properties using a rich typing system as a guide. Having related our proposal for such an expanded framework \LambdaTYn, we present some recent advances in the logical formalisms associated, including constraints on lexical transformations and polymorphic quantifiers, and ongoing discussions and research on the granularity of the type system and the limits of transitivity.

cs.CL↗

arXiv2013

Sémantique des déterminants dans un cadre richement typé

The variation of word meaning according to the context leads us to enrich the type system of our syntactical and semantic analyser of French based on categorial grammars and Montague semantics (or lambda-DRT). The main advantage of a deep semantic analyse is too represent meaning by logical formulae that can be easily used e.g. for inferences. Determiners and quantifiers play a fundamental role in the construction of those formulae. But in our rich type system the usual semantic terms do not work. We propose a solution ins- pired by the tau and epsilon operators of Hilbert, kinds of generic elements and choice functions. This approach unifies the treatment of the different determi- ners and quantifiers as well as the dynamic binding of pronouns. Above all, this fully computational view fits in well within the wide coverage parser Grail, both from a theoretical and a practical viewpoint.

cs.CL↗