Structures grammaticales dans le français mathématique : I

Ranta, Aarne

Mathématiques informatique et sciences humaines, Tome 138 (1997), pp. 5-56.

Un système de règles grammaticales est présenté pour analyser un fragment du français permettant l'expression de théorèmes et de preuves mathématiques. Pour cet objectif, on développe une version de la grammaire de Montague, avec des catégories syntaxiques relatives au contexte et aux domaines d'individus. Ce système peut être interprété dans la théorie constructive des types de Martin-Löf. Il est appliqué, d'abord, au français sans symboles mathématiques, avec une attention spéciale aux restrictions de sélection et aux dépendances par rapport à un contexte. Le fragment comprend des verbes et des adjectifs, des formes plurielles, des propositions relatives, et des syntagmes coordonnés. Ensuite, la grammaire est étendue au symbolisme mathématique et à son usage dans le texte français. Le fragment comprend des formules arithmétiques, la notation décimale, les conventions de parenthèses, les variables explicites, des énoncés de théorèmes et des structures textuelles de preuves. On finit par étudier quelques applications de la grammaire, basées sur l'implémentation déclarative de la grammaire dans ALF, un éditeur de preuves.

A system of grammatical rules is presented to analyse a fragment of French that permits the expression of mathematical theorems and proofs. To this end, a version of Montague grammar is developed, with syntactic categories relativized to a context and to domains of individuals. This system can be interpreted in the constructive type theory of Martin-Löf. It is first applied to French without mathematical symbols, paying special attention to selectional restrictions and to dependencies on context. The fragment includes verbs and adjectives, plurals, relative clauses, and coordinated phrases of different categories. Second, the grammar is extended to mathematical symbolism and its embedding in French text. The fragment comprises arithmetical formulae, decimal notation, parenthesis conventions, explicit variables, statements of theorems, and textual structures of proofs. Finally, some applications of the grammar are studied, based on a declarative implementation in the proof editor ALF.

Abeillé A., Les nouvelles syntaxes, Paris, Armand Colin, 1993.

Ajdukiewicz K., «Die syntaktische Konnexität », Studia Philosophica 1 (1935), pp. 1-27. | JFM | Zbl

Bar-Hillel Y., «A quasi-arithmetical notation for syntactic description », Language, 29 (1953), pp. 47-58. | Zbl

De Bruijn N.G., «Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem », Indagationes Mathematicae 34 (1972), pp. 381-392. | MR | Zbl

De Bruijn N.G., « The mathematical vernacular, a language for mathematics with typed sets », NEDERPELT R., éd., Selected Papers on Automath, pp. 865-935, Amsterdam, North-Holland, 1994. | MR

Chambreuil M., Grammaire de Montague: langage, traduction, interprétation, ADOSA, Clermont-Ferrand, 1989. | MR

Chomsky N., Aspects of the Theory of Syntax, Cambridge, Ma., The M.I.T. Press, 1965.

Coscoy Y., Kahn G. et Théry L., Extracting text from proofs, Rapport de recherche n. 2459, Sophia-Antipolis, INRIA, 1995. | MR

Frege G., Begriffsschrift, Halle A/S, Louis Nebert, 1879. | JFM

Gazdar G., Klein E., Pullum G. et Sag I., Generalized Phrase Structure Grammar, Oxford, Basil Blackwell, 1985.

Geach P., Reference and Generalit y, Ithaca, New York, Cornell University Press, 1962.

Gentzen G., « Untersuchungen über das logische Schliessen », Mathematische Zeitschrift, 39 (1934), pp. 176-210 et 405-431. | JFM | Zbl

Grevisse M., Le bon usage, Treizième édition, Paris, Duculot, 1993.

Heyting A., Intuititionism, Amsterdam, North-Holland, 1956. | MR | Zbl

Lambek J., «The mathematics of sentence structure », American Mathematical Monthly, 65 (1958), pp. 154-170. | MR | Zbl

Lamport L., LATEX. A Document Preparation System, Reading, Ma., Addison-Wesley Publishing Company, 1986.

Lecomte A., Modèles logiques en théorie linguistique, Synthèse de travaux présentés en vue de l'habilitation à diriger des recherches, Université de Grenoble, 1994.

Magnusson L., The Implementation of ALF - a Proof Editor Based on Martin-Löf's Monomorphic Type Theory with Explicit Substitutions, Thèse doctorale, Department of Computing Science, University of Göteborg, 1994.

Martin-Löf P., Intuitionistic Type Theory, Naples, Bibliopolis, 1984. | MR | Zbl

Montague R., Formal Philosophy, Collected papers edited by R.. THOMASON, New Haven, Yale University Press, 1974.

Morrill G., Type Logical Crammar, Dordrecht, Kluwer Academic Publishers, 1994. | Zbl

Nordström B., Petersson K. et Smith J., Programming in Martin-Löf's Type Theory. An Introduction, Oxford, Clarendon Press, 1990. | MR | Zbl

Paulson L., ML for the Working Programmer, Cambridge, Cambridge University Press, 1991. | Zbl

Von Plato J., «The axioms of constructive geometry», Annals of Pure and Applied Logic, 76 (1995), pp. 169-200. | MR | Zbl

Ranta A., Type Theoretical Grammar, Oxford, Oxford University Press, 1994. | Zbl

Ranta A., « Syntactic categories in the language of mathematics », DYBJER P., NORDSTRÖM B. et SMITH J., éd., Types for Proofs and Programs, pp. 162-182, Lecture Notes in Computer Science 996, Heidelberg, Springer-Verlag, 1995. | MR

Ranta A., « Context-relative syntactic categories and the formalization of mathematical text », BERARDI S. et COPPO M., éd., Types for Proofs and Programs, pp. 231-248, Lecture Notes in Computer Science 1158, Heidelberg, Springer-Verlag, 1996. | MR

Shieber S., An Introduction to Unification-Based Approaches to Grammar, Menlo Park, Ca., CSLI, 1986. | Zbl

Steedman M., « Combinators and grammars », OEHRLE R., BACH E. et WHEELER D., éd., Categorial Grammars and Natural Language Structures, pp. 417-442, Dordrecht, D. Reidel,1988.

Tasistro A., Formulation of Martin-Löf's Monomorphic Theory of Types with Explicit Substitutions, Thèse de licence, Department of Computing Science, University of Göteborg, 1993.