Structures grammaticales dans le français mathématique : II - (suite et fin)
Ranta, Aarne
Mathématiques et Sciences humaines, Tome 140 (1997), p. 5-36 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU)

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 mathetimatical 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.

Publié le : 1997-01-01
@article{MSH_1997__139__5_0,
     author = {Ranta, Aarne},
     title = {Structures grammaticales dans le fran\c cais math\'ematique : II - (suite et fin)},
     journal = {Math\'ematiques et Sciences humaines},
     volume = {140},
     year = {1997},
     pages = {5-36},
     mrnumber = {1600696},
     zbl = {0891.03008},
     language = {fr},
     url = {http://dml.mathdoc.fr/item/MSH_1997__139__5_0}
}

Ranta, Aarne. Structures grammaticales dans le français mathématique : II - (suite et fin). Mathématiques et Sciences humaines, Tome 140 (1997) pp. 5-36. http://gdmltest.u-ga.fr/item/MSH_1997__139__5_0/

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

Ajdukiewicz K., «Die syntaktische Konnexitat », Studia Philosophica 1 (1935), pp. 1-27. | JFM 62.1050.03 | Zbl 0015.33702

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

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 321704 | Zbl 0253.68007

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 1429429

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

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 1477978

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

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

Geach P., Reference and Generality, 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 60.0846.01 | Zbl 0010.14601

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

Heyting A., Intuitionism. Amsterdam, North-Holland, 1956. | MR 75147 | Zbl 0070.00801

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

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 Goteborg, 1994.

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

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

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

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

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

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

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

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 1456764

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 1474542

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

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 Goteborg, 1993.