The Displacement Calculus

If all dependent expressions were adjacent some variety of immediate constituent analysis would suffice for grammar, but syntactic and semantic mismatches are characteristic of natural language; indeed this is a, or the, central problem in grammar. Logical categorial grammar reduces grammar to logic: an expression is well-formed if and only if an associated sequent is a theorem of a categorial logic. The paradigmatic categorial logic is the Lambek calculus, but being a logic of concatenation the Lambek calculus can only capture discontinuous dependencies when they are peripheral. In this paper we present the displacement calculus, which is a logic of intercalation as well as concatenation and which subsumes the Lambek calculus. On the empirical side, we apply the new calculus to discontinuous idioms, quantification, VP ellipsis, medial extraction, pied-piping, appositive relativisation, parentheticals, gapping, comparative subdeletion, cross-serial dependencies, reflexivization, anaphora, dative alternation, and particle shift. On the technical side, we prove that the calculus enjoys Cut-elimination.     

A New Correctness Criterion for Cyclic Proof Nets

We define proof nets for cyclic multiplicative linear logic as edge bi-coloured graphs. Our characterization is purely graph theoretical and works without further complication for proof nets with cuts, which are usually harder to handle in the non-commutative case. This also provides a new characterization of the proof nets for the Lambek calculus (with the empty sequence) which simply are a restriction on the formulas to be considered (which are asked to be intuitionistic).     

A modular and parameterized presentation of pregroup calculus

The concept of pregroup was introduced by Lambek for natural language analysis, with a close link to non-commutative linear logic. We reformulate the pregroup calculus so as to extend it by composition with other logics and calculi. The cut elimination property and the decidability property of the sequent calculus proposed in the article are shown. Properties of composed calculi are also discussed.     

Syntactic Calculus with Dependent Types

The aim of this study is to look at the the syntactic calculus of Bar-Hillel and Lambek, including semantic interpretation, 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 Lambek calculus. 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 of constructive type theory.Two alternative formalizations are given: one using syntax trees, like Montague grammar, and one dispensing with them, like the theory called minimalistic by Morrill. The syntax tree approach is presented as the main alternative, because it makes it possible to embed the calculus in a more extensive Montague-style grammar.     

Multimodal linguistic inference

In this paper we compare grammatical inference in the context of simple and of mixed Lambek systems. Simple Lambek systems are obtained by taking the logic of residuation for a family of multiplicative connectives /,,\, together with a package of structural postulates characterizing the resource management properties of the connective.Different choices for Associativity and Commutativity yield the familiar logics NL, L, NLP, LP. Semantically, a simple Lambek system is a unimodal logic: the connectives get a Kripke style interpretation in terms of a single ternary accessibility relation modeling the notion of linguistic composition for each individual system.The simple systems earch have their virtues in linguistic analysis. But none of them in isolation provides a basis for a full theory of grammar. In the second part of the paper, we consider two types of mixed Lambek systems.The first type is obtained by combining a number of unimodal systems into one multimodal logic. The combined multimodal logic is set up in such a way that the individual resource management properties of the constituting logics are preserved. But the inferential capacity of the mixed logic is greater than the sum of its component parts through the addition of interaction postulates, together with the corresponding interpretive constraints on frames, regulating the communication between the component logics.The second type of mixed system is obtained by generalizing the residuation scheme for binary connectives to families of n-ary connectives, and by putting together families of different arities in one logic. We focus on residuation for unary connectives, and their combination with the standard binary vocabulary. The unary connectives play the role of control devices, both with respect to the static aspects of linguistic structure, and the dynamic aspects of putting this structure together. We prove a number of elementary logical results for unary families of residuated connectives and their combination with binary families, and situate existing proposals for structural modalities within a more general framework.An earlier version of the paper (under the title Residuation in mixed Lambek systems) was presented at the Deduction and Language workshop, London, March 1994, and the Rome workshop on Lambek Calculus, May 1994, and appeared in the IGPL Bulletin special issue Deduction and Language (Kempson (ed), Vol 3, 2–3). The materials in this paper prepare the ground for the sections on multiplicative connectives in a chapter on categorial grammar for the Handbook of Logic and Language (Van Benthem and ter Meulen (eds), Elsevier, to appear). I thank the editors of the Handbook and the audiences at these workshops for comments. I have greatly benefited from discussion, and joint work, with Natasha Kurtonina, Glyn Morrill and Dick Oehrle. All errors are my own.     

Displacement logic for anaphora

The displacement calculus of Morrill, Valentín and Fadda (2011) [25] aspires to replace the calculus of Lambek (1958) [13] as the foundation of categorial grammar by accommodating intercalation as well as concatenation while remaining free of structural rules and enjoying Cut-elimination and its good corollaries. Jäger (2005) [11] proposes a type logical treatment of anaphora with syntactic duplication using limited contraction. Morrill and Valentín (2010) [24] apply (modal) displacement calculus to anaphora with lexical duplication and propose extension with a negation as failure in conjunction with additives to capture binding conditions. In this paper we present an account of anaphora developing characteristics and employing machinery from both of these proposals.     

Language-Theoretic and Finite Relation Models for the (Full) Lambek Calculus

We prove completeness for some language-theoretic models of the full Lambek calculus and its various fragments. First we consider syntactic concepts and syntactic concepts over regular languages, which provide a complete semantics for the full Lambek calculus \({\mathbf {FL}}_\perp \). We present a new semantics we call automata-theoretic, which combines languages and relations via closure operators which are based on automaton transitions. We establish the completeness of this semantics for the full Lambek calculus via an isomorphism theorem for the syntactic concepts lattice of a language and a construction for the universal automaton recognizing the same language. Finally, we use automata-theoretic semantics to prove completeness of relation models of binary relations and finite relation models for the Lambek calculus without and with empty antecedents (henceforth: \(\mathbf L \) and \(\mathbf L1 \)), thus solving a problem left open by Pentus (Ann Pure Appl Log 75:179–213, 1995).     

Toward discourse representation via pregroup grammars

Every pregroup grammar is shown to be strongly equivalent to one which uses basic types and left and right adjoints of basic types only. Therefore, a semantical interpretation is independent of the order of the associated logic. Lexical entries are read as expressions in a two sorted predicate logic with ∈ and functional symbols. The parsing of a sentence defines a substitution that combines the expressions associated to the individual words. The resulting variable free formula is the translation of the sentence. It can be computed in time proportional to the parsing structure. Non-logical axioms are associated to certain words (relative pronouns, indefinite article, comparative determiners). Sample sentences are used to derive the characterizing formula of the DRS corresponding to the translation.     

基于轻语义λ-演算的汉语陈述句灵活语序研究

目前,自然语言处理已经从句法、语法层面走向轻语义层面。对于汉语陈述句的处理,传统的方法是采用Lambek演算来进行处理。但是传统的Lambek演算无法处理汉语中的灵活语序问题,而现有的方法,如加入模态词、新连接词等,又因为其进一步使得本已是NP-hard的Lambek演算时间复杂度变大,并不适合当前的计算机处理。基于此,该文提出了λ-Lambek演算,即采用Lambek演算来对汉语陈述句进行句法演算,并通过Curry-Howard对应理论与λ-演算来对汉语陈述句进行轻语义模型的构建。λ-Lambek演算不仅能够对汉语陈述句进行轻语义演算,而且还能对汉语陈述句灵活语序进行处理。     

Semantic Bootstrapping of Type-Logical Grammar

A two-stage procedure is described which induces type-logical grammar lexicons from sentences annotated with skeletal terms of the simply typed lambda calculus. First, a generalized formulae-as-types correspondence is exploited to obtain all the type-logical proofs of the sample sentences from their lambda terms. The resulting lexicons are then optimally unified. The first stage constitutes the semantic bootstrapping (Pinker, Language Learnability and Language Development, Harvard University Press, 1984), while the unification procedure of Buszkowski and Penn represents a first attempt at structure-dependent distributional learning of the syntactic and semantic categories. This effort extends earlier induction procedures (Buszkowski and Penn, 1990, Studia Logica 49, 431–454; Kanazawa, 1998, CSLI Publications and the European Association for Logic, Language and Information) for classical categorial grammar to at first the non-associative Lambek calculus, and then to a large class of type logics enriched by modal operators and structural rules.     

一种层次化的LSD规则体系及其分析算法

本文提出了一种基于词汇属性结构描述和规则继承的层次化LSD规则体系,讨论了该规则体系下的规则搜索策略和词汇化规则索引的实现方法,并在此基础上首次给出了LSD文法的非确定性分析算法。该规则系统具有从传统属性文法到现代词汇文法的可伸缩性,同时较好地解决了线性规则库中复杂的规则交互问题。     

Non-commutative logic III: focusing proofs

It is now well-established that the so-called focalization property plays a central role in the design of programming languages based on proof search, and more generally in the proof theory of linear logic. We present here a sequent calculus for non-commutative logic (NL) which enjoys the focalization property. In the multiplicative case, we give a focalized sequentialization theorem, and in the general case, we show that our focalized sequent calculus is equivalent to the original one by studying the permutabilities of rules for NL and showing that all permutabilities of linear logic involved in focalization can be lifted to NL permutabilities. These results are based on a study of the partitions of partially ordered sets modulo entropy.     

Semi-automatic documentation of an implemented linguistic grammar augmented with a treebank

We have constructed a large scale and detailed database of lexical types in Japanese from a treebank that includes detailed linguistic information. The database helps treebank annotators and grammar developers to share precise knowledge about the grammatical status of words that constitute the treebank, allowing for consistent large-scale treebanking and grammar development. In addition, it clarifies what lexical types are needed for precise Japanese NLP on the basis of the treebank. In this paper, we report on the motivation and methodology of the database construction.

On strict interpretations of grammar forms

Strict interpretations of grammar forms are studied with respect to parsing, ambiguity, and decidability for intersection and containment. In particular, a parsing procedure for an arbitrary strict interpretation grammar is given which is based on a given parsing method for the master grammar. Time and space bounds on the new procedure are then obtained. Each ambiguous interpretation grammar of an unambiguous grammar form can be converted to an equivalent unambiguous interpretation of the same grammar form. Unambiguity is always decidable for strict interpretation grammars of unambiguous grammar forms. Also, for languages obtained from compatible strict interpretations of an unambiguous grammar form, the following problems are solvable: empty intersection, finite intersection, containment, and equality.Portions of this paper were presented at (i) the 3rd ACM Symposium on Principles of Programming Languages, Jan. 1976, under the title, The Influence of Productions on Derivations and Parsing, and (ii) the 5th Symposium on Mathematical Foundations of Computer Science, Sept. 1976.This author was supported in part by a Guggenheim Fellowship and by NSF Grant No. 42306 and MCS 73-03380.This author was supported in part by NSF Grant No. MCS76-10076.     

Reasoning in Medical and Tutoring Systems: A Decidable First-Order Temporal Paraconsistent Non-Commutative Logic

Reasoning in medical and tutoring systems requires expressions relating not only to time-dependency, paraconsistency, constructiveness, and resource-sensitivity, but also order-sensitivity. Our objective in this study is to construct a decidable rst-order logic for appropriately expressing this reasoning. To meet this objective, we introduce a rst-order temporal paraconsistent non-commutative logic as a Gentzen-type sequent calculus. This logic has no structural rules but has some bounded temporal operators and a paraconsistent negation connective. The main result of this study is to show this logic to be decidable. Based on this logic, we present some illustrative examples for reasoning in medical and tutoring systems.     

结合结构下文及词汇信息的汉语句法分析方法

针对句法分析中上下文无关语法模型对句子信息利用的不足,通过融入结构下文和部分词汇信息,提出两种基于概率上下文无关语法模型的短语结构消歧方法,以达到消解结构歧义的目的;引入分层分析的算法,通过损失一定的时间效率使得在提高分析准确率的同时保证分析结果的全面性。实验结果表明,融入结构下文及词汇信息的汉语句法分析方法,利用了更多的句子信息,与上下文无关语法相比有着更强的消歧能力。     

基于模型的Fuzzing测试脚本自动化生成

针对基于知识的Fuzzing测试技术存在脚本编写工作量大的问题,提出一种基于模型的Fuzzing测试脚本自 动生成方法。方法首先以高阶属性文法形式化地描述数据模型,获取统一的、与测试环境无关的数据格式描述;然后 依据文法模型,将样本解析为带格式知识的文法分析树;最后建立文法分析树与测试逻辑的关联关系,实现自动化的 测试脚本生成。实验结果表明,所提出的方法能够自动生成有效的测试脚本,并发现软件中潜在的安全漏洞。     

A ‘Natural Logic’ inference system using the Lambek calculus

This paper develops an inference system for natural language within the ‘Natural Logic’ paradigm as advocated by van Benthem (1997), Sánchez (1991) and others. The system that we propose is based on the Lambek calculus and works directly on the Curry-Howard counterparts for syntactic representations of natural language, with no intermediate translation to logical formulae. The Lambek-based system we propose extends the system by Fyodorov et~al. (2003), which is based on the Ajdukiewicz/Bar-Hillel (AB) calculus Bar Hillel, (1964). This enables the system to deal with new kinds of inferences, involving relative clauses, non-constituent coordination, and meaning postulates that involve complex expressions. Basing the system on the Lambek calculus leads to problems with non-normalized proof terms, which are treated by using normalization axioms.