Structures grammaticales dans le français mathématique : II - (suite et fin)
Mathématiques et Sciences Humaines (1997)
- Volume: 139, page 5-36
- ISSN: 0987-6936
Access Full Article
topAbstract
topHow to cite
topRanta, 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- Abeillé A., Les nouvelles syntaxes, Paris, Armand Colin, 1993.
- Ajdukiewicz K., «Die syntaktische Konnexitat », Studia Philosophica1 (1935), pp. 1-27. Zbl0015.33702JFM62.1050.03
- Bar-Hillel Y., « A quasi-arithmetical notation for syntactic description », Language, 29 (1953), pp. 47-58. Zbl0156.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 Mathematicae34 (1972), pp. 381-392. Zbl0253.68007MR321704
- 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
- Chambreuil M., Grammaire de Montague: langage, traduction, interprétation, ADOSA, Clermont-Ferrand, 1989. MR1196228
- 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. Zbl1063.68647MR1477978
- Frege G., Begriffsschrift, Halle A/S, Louis Nebert,1879. JFM11.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. Zbl0010.14601JFM60.0846.01
- Grevisse M., Le bon usage, Treizième édition, Paris, Duculot, 1993.
- Heyting A., Intuitionism. Amsterdam, North-Holland, 1956. Zbl0070.00801MR75147
- Lambek J., «The mathematics of sentence structure », AmericanAlathematical Monthly, 65 (1958), pp. 154-170. Zbl0080.00702MR106170
- 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. Zbl0571.03030MR769301
- 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. Zbl0848.03007
- Nordström B., Petersson K. et Smith J., Programming in Martin-Löf's Type Theory. An Introduction, Oxford, Clarendon Press, 1990. Zbl0744.03029MR1243882
- Paulson L., ML for the Working Programmer, Cambridge, Cambridge University Press, 1991. Zbl0746.68019
- Von Plato J., « The axioms of constructive geometry », Annals of Pure and Applied Logic, 76 (1995), pp. 169-200. Zbl0836.03034MR1361484
- Ranta A., Type Theoretical Grammar, Oxford, Oxford University Press, 1994. Zbl0855.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 Science996, Heidelberg, Springer-Verlag, 1995. MR1456764
- 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
- Shieber S., An Introduction to Unification-Based Approaches to Grammar, Menlo Park, Ca., CSLI, 1986. Zbl0770.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.
NotesEmbed ?
topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.