On the system F as a glue language for natural-language compositional-semantics

TL;DR

This paper advocates for using system F, a polymorphic lambda calculus, as a flexible framework for modeling natural language semantics, especially for lexical pragmatics, comparing it to alternative type theories.

Contribution

It provides a detailed rationale for choosing system F over Martin-Löf's type theory in modeling compositional semantics of natural language.

Findings

System F effectively models lexical pragmatics phenomena.

System F offers advantages over Martin-Löf's type theory for semantic composition.

The paper clarifies the motivations behind selecting system F for semantic modeling.

Abstract

In order to model in compositional framework some phenomena of lexical pragmatics and in particular the ones studied by Nicholas Asher several contributions developed in our team did use the system F of Jean-Yves Girard to construct logical formulae expressing the meaning of sentences --- while other authors prefer to use Per Martin-L\"of's type theory In this note we explain the motivations supporting our preference for system F.