Structures grammaticales dans le français mathématique : II - (suite et fin)

Aarne Ranta

Mathématiques et Sciences Humaines (1997)

  • Volume: 139, page 5-36
  • ISSN: 0987-6936

Abstract

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

How to cite

top

Ranta, Aarne. "Structures grammaticales dans le français mathématique : II - (suite et fin)." Mathématiques et Sciences Humaines 139 (1997): 5-36. <http://eudml.org/doc/94502>.

@article{Ranta1997,
abstract = {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.},
author = {Ranta, Aarne},
journal = {Mathématiques et Sciences Humaines},
keywords = {fragment of French; Montague grammar; constructive type theory; mathematical symbolism; textual structures of proofs; declarative implementation in the proof editor ALF},
language = {fre},
pages = {5-36},
publisher = {Ecole des hautes-études en sciences sociales},
title = {Structures grammaticales dans le français mathématique : II - (suite et fin)},
url = {http://eudml.org/doc/94502},
volume = {139},
year = {1997},
}

TY - JOUR
AU - Ranta, Aarne
TI - Structures grammaticales dans le français mathématique : II - (suite et fin)
JO - Mathématiques et Sciences Humaines
PY - 1997
PB - Ecole des hautes-études en sciences sociales
VL - 139
SP - 5
EP - 36
AB - 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.
LA - fre
KW - fragment of French; Montague grammar; constructive type theory; mathematical symbolism; textual structures of proofs; declarative implementation in the proof editor ALF
UR - http://eudml.org/doc/94502
ER -

References

top
  1. Abeillé A., Les nouvelles syntaxes, Paris, Armand Colin, 1993. 
  2. Ajdukiewicz K., «Die syntaktische Konnexitat », Studia Philosophica1 (1935), pp. 1-27. Zbl0015.33702JFM62.1050.03
  3. Bar-Hillel Y., « A quasi-arithmetical notation for syntactic description », Language, 29 (1953), pp. 47-58. Zbl0156.25402
  4. De Bruijn N.G., « Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem », Indagationes Mathematicae34 (1972), pp. 381-392. Zbl0253.68007MR321704
  5. 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. MR1429429
  6. Chambreuil M., Grammaire de Montague: langage, traduction, interprétation, ADOSA, Clermont-Ferrand, 1989. MR1196228
  7. Chomsky N., Aspects of the Theory of Syntax, Cambridge, Ma., The M.I.T. Press, 1965. 
  8. Coscoy Y., Kahn G. et Théry L., Extracting text from proofs, Rapport de recherche n. 2459, Sophia-Antipolis, INRIA,1995. Zbl1063.68647MR1477978
  9. Frege G., Begriffsschrift, Halle A/S, Louis Nebert,1879. JFM11.0048.02
  10. Gazdar G., Klein E., Pullum G. et Sag I., Generalized Phrase Structure Grammar, Oxford, Basil Blackwell, 1985. 
  11. Geach P., Reference and Generality, Ithaca, New York, Cornell University Press, 1962. 
  12. Gentzen G., « Untersuchungen über das logische Schliessen », Mathematische Zeitschrift, 39 (1934), pp. 176-210 et 405-431. Zbl0010.14601JFM60.0846.01
  13. Grevisse M., Le bon usage, Treizième édition, Paris, Duculot, 1993. 
  14. Heyting A., Intuitionism. Amsterdam, North-Holland, 1956. Zbl0070.00801MR75147
  15. Lambek J., «The mathematics of sentence structure », AmericanAlathematical Monthly, 65 (1958), pp. 154-170. Zbl0080.00702MR106170
  16. Lamport L., LATEX. A Document Preparation System, Reading, Ma., Addison-Wesley Publishing Company, 1986. 
  17. 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. 
  18. 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. 
  19. Martin-Löf P., lntuitionistic Type Theory, Naples, Bibliopolis, 1984. Zbl0571.03030MR769301
  20. Montague R., Formal Philosophy, Collected papers edited by R. THOMASON, New Haven, Yale University Press, 1974. 
  21. Morrill G., Type Logical Grammar, Dordrecht, Kluwer Academic Publishers, 1994. Zbl0848.03007
  22. Nordström B., Petersson K. et Smith J., Programming in Martin-Löf's Type Theory. An Introduction, Oxford, Clarendon Press, 1990. Zbl0744.03029MR1243882
  23. Paulson L., ML for the Working Programmer, Cambridge, Cambridge University Press, 1991. Zbl0746.68019
  24. Von Plato J., « The axioms of constructive geometry », Annals of Pure and Applied Logic, 76 (1995), pp. 169-200. Zbl0836.03034MR1361484
  25. Ranta A., Type Theoretical Grammar, Oxford, Oxford University Press, 1994. Zbl0855.68073
  26. 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 Science996, Heidelberg, Springer-Verlag, 1995. MR1456764
  27. 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 Science1158, Heidelberg, Springer-Verlag, 1996. MR1474542
  28. Shieber S., An Introduction to Unification-Based Approaches to Grammar, Menlo Park, Ca., CSLI, 1986. Zbl0770.68008
  29. 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. 
  30. 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. 

NotesEmbed ?

top

You must be logged in to post comments.