Paper Info
Title
Syntactic Calculus with Dependent Types
Abstract
The aim of this study is to look at the the syntactic calculus of Bar-Hillel and Lambek, including semanticinterpretation, from the point of view of constructive type theory. The syntactic calculus is given a formalization that makes it possible to implement it in a type-theoretical proof editor. Such an implementation combines formal syntax and formal semantics, and makes the type-theoretical tools of automatic and interactive reasoning available in grammar.In the formalization, the use of the dependent types of constructive type theory is essential. Dependent types are already needed in the semantics of ordinary Lambekcalculus. But they also suggest some natural extensions of the calculus,which are applied to the treatment of morphosyntactic dependencies and to an analysis of selectional restrictions. Finally, directed dependent function types are introduced, corresponding to the Π types ofconstructive type theory.Two alternative formalizations are given: one using syntax trees, like Montague grammar, and one dispensing with them, like thetheory called minimalistic by Morrill. The syntax tree approach ispresented as the main alternative, because it makes it possible to embed the calculus in a more extensive Montague-style grammar.
Year
DOI
Venue
1998
10.1023/A:1008390927185
Journal of Logic, Language and Information
Keywords
DocType
Volume
Constructive type theory,Lambek calculus,proof editors
Journal
7
Issue
ISSN
Citations 
4
1572-9583
0
PageRank 
References 
Authors
0.34
1
1
Name
Order
Citations
PageRank
Aarne Ranta131636.02