Book contents
- Frontmatter
- Contents
- List of contributors
- Preface
- 1 Determinacy in a synchronous π-calculus
- 2 Classical coordination mechanisms in the chemical model
- 3 Sequential algorithms as bistable maps
- 4 The semantics of dataflow with firing
- 5 Kahn networks at the dawn of functional programming
- 6 A simple type-theoretic language: Mini-TT
- 7 Program semantics and infinite regular terms
- 8 Algorithms for equivalence and reduction to minimal form for a class of simple recursive equations
- 9 Generalized finite developments
- 10 Semantics of program representation graphs
- 11 From Centaur to the Meta-Environment: a tribute to a great meta-technologist
- 12 Towards a theory of document structure
- 13 Grammars as software libraries
- 14 The Leordo computation system
- 15 Theorem-proving support in programming language semantics
- 16 Nominal verification of algorithm W
- 17 A constructive denotational semantics for Kahn networks in Coq
- 18 Asclepios: a research project team at INRIA for the analysis and simulation of biomedical images
- 19 Proxy caching in split TCP: dynamics, stability and tail asymptotics
- 20 Two-by-two static, evolutionary, and dynamic games
- 21 Reversal strategies for adjoint algorithms
- 22 Reflections on INRIA and the role of Gilles Kahn
- 23 Can a systems biologist fix a Tamagotchi?
- 24 Computational science: a new frontier for computing
- 25 The descendants of Centaur: a personal view on Gilles Kahn's work
- 26 The tower of informatic models
- References
13 - Grammars as software libraries
Published online by Cambridge University Press: 06 August 2010
By
Book contents
- Frontmatter
- Contents
- List of contributors
- Preface
- 1 Determinacy in a synchronous π-calculus
- 2 Classical coordination mechanisms in the chemical model
- 3 Sequential algorithms as bistable maps
- 4 The semantics of dataflow with firing
- 5 Kahn networks at the dawn of functional programming
- 6 A simple type-theoretic language: Mini-TT
- 7 Program semantics and infinite regular terms
- 8 Algorithms for equivalence and reduction to minimal form for a class of simple recursive equations
- 9 Generalized finite developments
- 10 Semantics of program representation graphs
- 11 From Centaur to the Meta-Environment: a tribute to a great meta-technologist
- 12 Towards a theory of document structure
- 13 Grammars as software libraries
- 14 The Leordo computation system
- 15 Theorem-proving support in programming language semantics
- 16 Nominal verification of algorithm W
- 17 A constructive denotational semantics for Kahn networks in Coq
- 18 Asclepios: a research project team at INRIA for the analysis and simulation of biomedical images
- 19 Proxy caching in split TCP: dynamics, stability and tail asymptotics
- 20 Two-by-two static, evolutionary, and dynamic games
- 21 Reversal strategies for adjoint algorithms
- 22 Reflections on INRIA and the role of Gilles Kahn
- 23 Can a systems biologist fix a Tamagotchi?
- 24 Computational science: a new frontier for computing
- 25 The descendants of Centaur: a personal view on Gilles Kahn's work
- 26 The tower of informatic models
- References
Summary
Abstract
Grammars of natural languages are needed in programs such as natural language interfaces and dialogue systems, but also more generally, in software localization. Writing grammar implementations is a highly specialized task. For various reasons, no libraries have been available to ease this task. This paper shows how grammar libraries can be written in GF (Grammatical Framework), focusing on the software engineering aspects rather than the linguistic aspects. As an implementation of the approach, the GF Resource Grammar Library currently comprises ten languages. As an application, a translation system from formalized mathematics to text in three languages is outlined.
Introduction
How can we generate natural language text from a formal specification of meaning, such as a formal proof? Coscoy, Kahn and Théry studied the problem and built a program that worked for all proofs constructed in the Coq proof assistant. Their program translates structural text components, such as we conclude that, but leaves propositions expressed in formal language:
We conclude that Even(n) → Odd(Succ(n)).
A similar decision is made in Isar, whereas Mizar permits English-like expressions for some predicates. One reason for stopping at this level is certainly that typical users of proof systems are comfortable with reading logical formulas, so that only the proof-level formalization needs translation.
- Type
- Chapter
- Information
- From Semantics to Computer ScienceEssays in Honour of Gilles Kahn, pp. 281 - 308Publisher: Cambridge University PressPrint publication year: 2009
References
[2], and . Verification of Object-Oriented Software: The KeY Approach, volume 4334 Lecture Notes in Computer Science. Springer-Verlag, 2006.Google Scholar
[3] and . Rapid prototyping of scalable grammars: Towards modularity in extensions to a language-independent core. In Proceedings of the 2nd International Joint Conference on Natural Language Processing IJCNLP-05 (Posters/Demos), Jeju Island, Korea, 2005.Google Scholar
[5]. Embedded Grammars. MSc Thesis, Department of Computing Science, Chalmers University of Technology, 2004.
[6] and . Translating Formal Software Specifications to Natural Language / A Grammar-Based Approach. In , , and (eds) Logical Aspects of Computational Linguistics (LACL 2005), volume 3402 LNCS/LNAI, pp. 51–66. Springer-Verlag, 2005.Google Scholar
[7], , , and . The Parallel Grammar Project. In COLING 2002, Workshop on Grammar Engineering and Evaluation, pp. 1–7, 2002.Google Scholar
[8]. WebALT! Deliver Mathematics Everywhere. In Proceedings of SITE 2006. Orlando March 20–24, 2006.Google Scholar
[9]. Explication textuelle de preuves pour le calcul des constructions inductives. PhD thesis, Université de Nice-Sophia-Antipolis, 2000.
[10], and . Extracting text from proofs. In and (eds) Proc. Second International Conference on Typed Lambda Calculi and Applications, volume 902 Lecture Notes in Computer Science, pp. 109–123, Springer-Verlag, 1995.Google Scholar
[11]. Some logical aspects of grammatical structure. In , editor, Structure of Language and its Mathematical Aspects: Proceedings of the Twelfth Symposium in Applied Mathematics, pp. 56–68. American Mathematical Society, 1963.Google Scholar
[12]. Towards abstract categorial grammars. In Association for Computational Linguistics, 39th Annual Meeting and 10th Conference of the European Chapter, Toulouse, France, pp. 148–155, 2001.Google Scholar
[13]. Implementation of the Arabic numerals and their syntax in GF. In Computational Approaches to Semitic Languages: Common Issues and Resources, ACL-2007 Workshop, June 28, 2007, Prague, 2007.Google Scholar
[14] and . Implementing an open source arabic resource grammar in GF. In (ed.) Perspectives on Arabic Linguistics XX, pp. 209–232. John Benjamins, Amsterdam and Philadelphia, 2007.Google Scholar
[16] and . An extensible proof text editor. In and (eds) LPAR-2000, volume 1955 LNCS/LNAI, pp. 70–84. Springer, 2000.Google Scholar
[17]. A functional toolkit for morphological and phonological processing, application to a Sanskrit tagger. Journal of Functional Programming, 15(4):573–614, 2005.Google Scholar
[18]. Urdu Morphology, Orthography and Lexicon Extraction. MSc Thesis, Department of Computing Science, Chalmers University of Technology, 2006.
[19]. GF parallel resource grammars and Russian. In Coling/ACL 2006, pp. 475–482, 2006.Google Scholar
[20]. Constructive mathematics and computer programming. In Cohen, Los, Pfeiffer and Podewski (eds) Logic, Methodology and Philosophy of Science VI, pp. 153–175. North-Holland, Amsterdam, 1982.Google Scholar
[21]. Formal Philosophy. Yale University Press, New Haven, 1974. Collected papers edited by R. Thomason.Google Scholar
[22]. Lambda grammars and the syntax-semantics interface. In and (eds) Proceedings of the Thirteenth Amsterdam Colloquium, pp. 150–155, Amsterdam, 2001.Google Scholar
[23] and . Dialogue System Localization with the GF Resource Grammar Library. In SPEECHGRAM 2007: ACL Workshop on Grammar-Based Approaches to Spoken Language Processing, June 29, 2007, Prague, 2007.Google Scholar
[24]. Higher-order categorial grammar. In (ed.) Proceedings of the Conference on Categorial Grammars (CG2004), Montpellier, France, pp. 340–361, 2004.Google Scholar
[25]. Grammatical framework: a type-theoretical grammar formalism. Journal of Functional Programming, 14(2):145–189, 2004.Google Scholar
[26]. Modular grammar engineering in GF. Research on Language and Computation, 5:133–158, 2007.Google Scholar
[27]. Grammatical Framework Homepage, 2008. digitalgrammars.com/gf.
[28], , , and . The Spoken Language Translator. Cambridge University Press, Cambridge, 2000.Google Scholar
[30]. The Coq Proof Assistant Reference Manual. pauillac.inria.fr/coq/, 1999.
[31]. The Mizar Homepage. http://mizar.org/, 2006.
[32]. Isar – a generic interpretative approach to readable formal proof documents. In , , , and (eds) Theorem Proving in Higher Order Logics, TPHOLs'99, volume 1690 Lecture Notes in Computer Science, 1999.Google Scholar
[33]. Formal proof sketches. In Types for Proofs and Programs, volume 3085 Lecture Notes in Computer Science, pp. 378–393. Springer, 2004.Google Scholar
- 6
- Cited by