Cut-Rule Axiomatization of the Syntactic Calculus L0

In Zielonka (1981a, 1989), I found an axiomatics for the product-free calculus L of Lambek whose only rule is the cut rule. Following Buszkowski (1987), we shall call such an axiomatics linear. It was proved that there is no finite axiomatics of that kind. In Lambek's original version of the calculus (cf. Lambek, 1958), sequent antecedents are non empty. By dropping this restriction, we obtain the variant L ₀ of L. This modification, introduced in the early 1980s (see, e.g., Buszkowski, 1985; Zielonka, 1981b), did not gain much popularity initially; a more common use of L ₀ has only occurred within the last few years (cf. Roorda, 1991: 29). In Zielonka (1988), I established analogous results for the restriction of L ₀ to sequents without left (or, equivalently, right) division. Here, I present a similar (cut-rule) axiomatics for the whole of L ₀. This paper is an extended, corrected, and completed version of Zielonka (1997). Unlike in Zielonka (1997), the notion of rank of an axiom is introduced which, although inessential for the results given below, may be useful for the expected non-finite-axiomatizability proof. The paper follows the same way of subject exposition as Zielonka (2000) but it is technically much less complicated. I restrict myself to giving bare results; all the ideological background is exactly the same as in case of the non-associative calculusNL ₀ and those who are interested in it are requested to consult the introductory section of Zielonka (2000). This revised version was published online in August 2006 with corrections to the Cover Date.     

Proof Nets for Basic Discontinuous Lambek Calculus

The theory of proof nets for continuity based on the Lambekcalculus is well-developed, but we need a compatible extensionto include discontinuity. Earlier work set out ingredients:hypersequent calculus and proof nets expanded with parameteredges. This article completes a preliminary line by finalizinga version of proof nets for the basic discontinuous Lambek calculusBDLC (the minimal system with one point of discontinuity) andproving correctness with respect to the hypersequent calculus.     

Proof Complexity of the Cut-free Calculus of Structures

We investigate the proof complexity of analytic subsystems ofthe deep inference proof system SKSg (the calculus of structures).Exploiting the fact that the cut rule (i) of SKSg correspondsto the ¬-left rule in the sequent calculus, we establishthat the ‘analytic'system KSg+c has essentially the samecomplexity as the monotone Gentzen calculus MLK. In particular,KSg+c quasipolynomially simulates SKSg, and admits polynomial-sizeproofs of some variants of the pigeonhole principle.     

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

Reference Constructions in the Single-conclusion Proof Logic

We propose an extension of the propositional proof logic languageby the second-order variables denoting the reference constructors(like ‘the formula which is proven by x’). The prooflogic in this weak second-order language is axiomatized viathe calculus _ref, the (Functional)Logic of Proofs with References. It is supplied with the formalarithmetical semantics: we prove that _ref is sound with respect to arithmetical interpretationsand is a conservative extension of propositional single-conclusionproof logic . Finally,we demonstrate how the language of _ref can be used as a scheme language for arithmetic and providethe corresponding proof conversion method.     

一类非线性系统的H2容错控制器的设计及其在空间飞行器的应用

针对存在执行器故障的不确定系统,本文研究了一种H2鲁棒容错控制的设计.控制器包括三个功能: 1)利用径向基函数(Radial basis function, RBF)神经网络估计得到的近似非线性函数构成闭环控制,抵消系统的非线性特征; 2)能实现H2性能指标的最优控制; 3)利用滑模控制抑制模型估计误差以提高控制精度, 并且控制器具有指定稳定裕度的设计功能.文中提出了用于执行器故障估计的调整规则, 故障估计信息用于控制律的设计.基于Lyapunov函数,推导了满足H2最优性能的充分条件:非线性二次矩阵不等式. 为了降低计算成本,给出了不等式求解的简化算法,避免了在线求解非线性矩阵不等式.通过一个空间飞行器模型的仿真, 验证了本文提出方法的有效性.     

On the Recognizing Power of the Lambek Calculus with Brackets

Every language recognized by the Lambek calculus with brackets is context-free. This is shown by combining an observation by Jäger with an entirely straightforward adaptation of the method Pentus used for the original Lambek calculus. The case of the variant of the calculus allowing sequents with empty antecedents is slightly more complicated, requiring a restricted use of the multiplicative unit.     

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.     

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

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

基于正则化的本征音说话人自适应方法

将正则化方法应用于本征音说话人自适应算法中,有效地解决了说话人子空间基的先验选择问题. 通过对似然函数引入适当的正则项,在优化过程中从候选本征音基矢量中自动选择最佳的本征音进行线性组合. 本文讨论了三种正则化因子,并给出了其数学优化算法. l1正则化可以得到说话人因子的稀疏解,其非零项即对应最佳本征音基矢量; l2正则化可以提高解的稳健性,在某种程度上减少了子空间维数的先验选择对识别率的影响;而弹性网正则化则通过线性组合在二者之间取得折衷.有监督说话人自适应实验表明,新方法与本征音方法的最好结果相比,在少量的自适应数据条件下(10s以下),识别率相对提高了近1%～2%.三种方法中, l1正则化略优于l2正则化,而在引入弹性网正则化后,系统性能有了进一步提高.     

Call-by-Value {lambda}-calculus and LJQ

LJQ is a focused sequent calculus for intuitionistic logic,with a simple restriction on the first premiss of the usualleft introduction rule for implication. In a previous paperwe discussed its history (going back to about 1950, or beyond)and presented its basic theory and some applications; here wediscuss in detail its relation to call-by-value reduction inlambda calculus, establishing a connection between LJQ and theCBV calculus _C of Moggi. In particular, we present an equationalcorrespondence between these two calculi forming a bijectionbetween the two sets of normal terms, and allowing reductionsin each to be simulated by reductions in the other.     

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.     

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.     

Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic

There has been a great deal of work on characterizing the complexityof the satisfiability and validity problem for modal logics.In particular, Ladner showed that the satisfiability problemfor all logics between K and S4 is PSPACE-hard, while for S5it is NP-complete. We show that it is negative introspection,the axiom ¬K_p K¬K_p, that causes the gap: if we addthis axiom to any modal logic between K and S4, then the satisfiabilityproblem becomes NP-complete. Indeed, the satisfiability problemis NP-complete for any modal logic that includes the negativeintrospection axiom.     

容错控制系统鲁棒H∞和自适应补偿设计

通过设计动态输出反馈控制策略研究线性时不变系统执行器故障下的鲁棒自适应容错H∞控制问题. 结合自适应技术和线性矩阵不等式(Linear matrix inequalities, LMI)技术, 设计一个控制策略同时实现系统的故障补偿控制和性能优化控制. 在设计中, 提出由自适应律在线调节控制增益方程补偿未知执行器故障和摄动; 并设计一个基于模式依赖李亚普诺夫方程的LMI条件解出控制参数及次优H∞性能. 所设计的动态输出反馈控制器可以处理一般执行器卡死故障, 并得到更少保守性的H∞性能指标. 此外, 一个更具挑战性的问题, 即通过自适应机构补偿故障致使系统多少性能退化得到论证. 所提方法的有效性由一个解耦线性化动态飞行器系统仿真验证.     

Computability in Specification

In reference (Foundation of specification. Journal of Logicand Computation, 15, 951–974, 2005), the author introducesa core specification theory (CST) in order to provide a logicalframework for the design and exploration of specification languages.In this article, we formulate two highly expressive extensionsof CST. The first (CST_U) is CST + a universe of types and thesecond (CST_US) permits specifications themselves to be dataitems. Finally, we shall explore their metamathematical propertiesand, in particular, provide an interpretation into first-orderarithmetic.     

在不准确方差下带随机系数矩阵的卡尔曼滤波稳定性

针对离散时间线性随机系统,研究了卡尔曼滤波的L2-稳定性问题. 考虑具有这两个特点的系统: 1)系数矩阵是随机的; 2)过程噪声、量测噪声、初始估计误差的方差矩阵不准确. 在系数矩阵有界、条件能观测、初始估计误差有界的假设下, 得到了卡尔曼滤波的L2-稳定性. 同时, 建立了卡尔曼滤波和状态空间最小二乘的等价性, 并在该等价性基础上得到状态空间最小二乘的状态估计误差L2-稳定性. 最后, 数值仿真说明了卡尔曼滤波的有效性.     

基于minmaxKKT条件的三维重构方法

机器视觉中, 三维重构是一个重要问题. 基于2范数的最小二乘法速度较快, 但因误差代价函数非凸, 理论上无法获得全局最优解, 即使通过分支限界等方法, 往往也只能获得局部最优. 无穷范数表示的误差代价函数理论上可以获得全局最优, 但是计算速度很慢. 本文提出一种基于最小最大库恩塔克条件(minmaxKKT)的三维重构方法. 该方法利用minmaxKKT条件对基于2范数的三维重构结果进行全局最优判别, 对陷入局部最优的结果运用混合最速下降法进行全局寻优. 该方法可以获得全局最优, 相对于无穷范数算法具有更高的计算效率. 对标准数据集和真实数据的实验结果证明了本文算法的可行性和优点.     

The Lambek calculus enriched with additional connectives

Some formal properties of enriched systems of Lambek calculus with analogues of conjunction and disjunction are investigated. In particular, it is proved that the class of languages recognizable by the Lambek calculus with added intersective conjunction properly includes the class of finite intersections of context-free languages.I would like to thank Professor Johan van Benthem for much encouragement and a number of helpful suggestions. Thanks are also due to Dirk Roorda, who commented on an earlier draft of the paper, and to my advisor Professor Stanley Peters.     

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.