Adjectival and Adverbial Modification: The View from Modern Type Theories

In this paper we present a study of adjectival/adverbial modification using modern type theories (MTTs), i.e. type theories within the tradition of Martin-Löf. We present an account of various issues concerning adjectival/adverbial modification and argue that MTTs can be used as an adequate language for interpreting NL semantics. MTTs are not only expressive enough to deal with a range of modification phenomena, but are furthermore well-suited to perform reasoning tasks that can be easily implemented (e.g. in proof-assistants) given their proof-theoretic nature. In MTT-semantics, common nouns are interpreted as types rather than predicates. Therefore, in order to capture the semantics of adjectives adequately, one needs to meet the challenge of modeling CNs modified by adjectives as types. To explicate that this can be done successfully, we first look at the mainstream classification of adjectives, i.e. intersective, subsective and non-subsective adjectives. There, we show that the rich type structure available in MTTs, along with a suitable subtyping framework, offers an adequate mechanism to model these cases. In particular, this modelling naturally takes care of the characterising inferences associated with each class of adjectives. Then, more advanced issues on adjectival modification are discussed: (a) degree adjectives, (b) comparatives and (c) multidimensional adjectives. There, it is shown that the use of indexed types can be usefully applied in order to deal with these cases. In the same vein, the issue of adverbial modification is discussed. We study two general typings for sentence and VP adverbs respectively. It is shown that the rich type structure in MTTs further provides useful organisational mechanisms in giving formal semantics for adverbs. In particular, we discuss the use of \(\varSigma \)-types to capture the veridicality/non-veridicality distinction and further discuss cases of intensional adverbs using the type theoretic notion of context (i.e. without resorting to intensional typing). We also look at manner, subject and speech act adverbials and propose solutions using MTTs. Finally, we show that the current proof technology can help mechanically check the associated inferences. A number of our proposals concerning adjectival and adverbial modification have been formalised in the proof assistant Coq and many of the associated inference patterns are checked to be correctly captured.     

Coinductive big-step operational semantics

Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We formalize the connections between the coinductive big-step semantics and the standard small-step semantics, proving that both semantics are equivalent. We then study the use of coinductive big-step semantics in proofs of type soundness and proofs of semantic preservation for compilers. A methodological originality of this paper is that all results have been proved using the Coq proof assistant. We explain the proof-theoretic presentation of coinductive definitions and proofs offered by Coq, and show that it facilitates the discovery and the presentation of the results.     

汉语形名复合词的语义建构: 基于物性结构与概念整合理论

该文用定量和定性分析相结合的方法,考察了现代汉语双音节形名复合词的物性修饰关系,发现形语素有选择地约束名语素的不同物性角色。当形语素修饰名语素的形式角色或构成角色时,语义解读时常需要补充名词;当形语素修饰名语素的施成角色、功用角色或规约化属性时,语义解读时常需要补充动词。形名复合词的语义建构是物性结构和概念整合共同作用的结果,当形语素激活的物性角色或物性值不止一个时,就会出现多义或歧义。
     

Meaning and Dialogue Coherence: A Proof-theoretic Investigation

This paper presents a novel proof-theoretic account of dialogue coherence. It focuses on an abstract class of cooperative information-oriented dialogues and describes how their structure can be accounted for in terms of a multi-agent hybrid inference system that combines natural deduction with information transfer and observation. We show how certain dialogue structures arise out of the interplay between the inferential roles of logical connectives (i.e., sentence semantics), a rule for transferring information between agents, and a rule for information flow between agents and their environment. The order of explanation is opposite in direction to that adopted in game-theoretic semantics, where sentence semantics (or a notion of valid inference) is derived from winning dialogue strategies. That approach and the current one may, however, be reconcilable, since we focus on cooperative dialogue, whereas the game-theoretic tradition concentrates on adversarial dialogue. An erratum to this article can be found at     

The Disconnection Tableau Calculus

In this paper we give a comprehensive presentation of the disconnection tableau calculus, a proof method for formulas in classical first-order clause logic. The distinguishing property of this calculus is that it uses unification in such a manner that important proof-theoretic advantages of the classical (i.e., Smullyan-style) tableau calculus are preserved, specifically the termination and model generation characteristics for certain formula classes. Additionally, the calculus is well suited for fully automated proof search. The calculus is described in detail with soundness and completeness proofs, and a number of important calculus refinements developed over the past years are presented. Referring to the model-finding abilities of the disconnection calculus, we explain the extraction and representation of models. We also describe the integration of paramodulation-based equality handling. Finally, we give an overview of related methods.     

A structured approach to static semantics correctness

An approach to the correctness proof of static semantics with respect to the standard semantics of a programming language is presented, where correctness means that the properties of the language described by the static semantics, such as type checking, are consistent with the standard semantics. The standard and static semantics are given in a denotational style in terms of some basic domains and domain constructors, which, together with suitable operations, are used to describe fundamental semantic concepts. The domains have different meaning in the two semantics and the static semantics correctness proof is carried out by devising a set of suitable functions between them. We show that the correctness proof can be greatly simplified by structuring the semantics definitions, and we illustrate that by applying the methodology to a simple imperative language. In the example the derivation of a static checking algorithm from the static semantics is described.     

A Modal Interpretation of the Logic of Interrogation

We propose a novel interpretation of natural-language questions using a modal predicate logic of knowledge. Our approach brings standard model-theoretic and proof-theoretic techniques from modal logic to bear on questions. Using the former, we show that our interpretation preserves Groenendijk and Stokhof's answerhood relation, yet allows an extensional interpretation. Using the latter, we get a sound and complete proof procedure for the logic for free. Our approach is more expressive; for example, it easily treats complex questions with operators that scope over questions. We suggest a semantic criterion that restricts what natural-language questions can express. We integrate and generalize much previous work on the semantics of questions, including Beck and Sharvit's families of subquestions, non-exhaustive questions, and multi-party conversations.     

A parametric approach to deductive databases with uncertainty

Numerous frameworks have been proposed in recent years for deductive databases with uncertainty. On the basis of how uncertainty is associated with the facts and rules in a program, we classify these frameworks into implication-based (IB) and annotation-based (AB) frameworks. We take the IB approach and propose a generic framework, called the parametric framework, as a unifying umbrella for IB frameworks. We develop the declarative, fixpoint, and proof-theoretic semantics of programs in our framework and show their equivalence. Using the framework as a basis, we then study the query optimization problem of containment of conjunctive queries in this framework and establish necessary and sufficient conditions for containment for several classes of parametric conjunctive queries. Our results yield tools for use in the query optimization for large classes of query programs in IB deductive databases with uncertainty     

ORDBMS中动态模式修改的研究

继承性是对象-关系型数据库管理系统(ORDBMS)的一个重要特征.它提供了强有力的增量建 模能力,也增加了模式演变的复杂度.通过对完全继承语义进行进一步的探讨,提出ORDBMS 中动态模式修改(dynamic schema modification,简称DSM)的准则化模型,并通过继承 层次选择表达式(inheritance hierarchy selective expression,简称IHSE)概念的引入,使 子类在超类模式改变时,可以自由地选择级联改变或迁移策略.     

一个机器检测的Micro-Dalvik虚拟机模型

给出了一个寄存器架构的虚拟机模型Micro-Dalvik,包括虚拟机指令集和虚拟机运行时状态的形式化,并以大步操作语义(big-step operational semantics)的方式给出了指令单步执行的状态转换以及定义在单步执行上的自反传递闭包来表达虚拟机程序的运行时状态转换.最后,以定理的形式描述了语义满足的性质,并得到证明.这个模型的指令集包括了大部分Dalvik虚拟机指令,为获得形式语义的清晰化,它在Dalvik VM指令集上进行了必要的抽象,对其实质没有改变,因而具有较大的实用性.该形式化模型通过了定理证明助手Isabelle/HOL的验证.     

Representing model theory in a type-theoretical logical framework

In a broad sense, logic is the field of formal languages for knowledge and truth that have a formal semantics. It tends to be difficult to give a narrower definition because very different kinds of logics exist. One of the most fundamental contrasts is between the different methods of assigning semantics. Here two classes can be distinguished: model theoretical semantics based on a foundation of mathematics such as set theory, and proof theoretical semantics based on an inference system possibly formulated within a type theory.Logical frameworks have been developed to cope with the variety of available logics unifying the underlying ontological notions and providing a meta-theory to reason abstractly about logics. While these have been very successful, they have so far focused on either model or proof theoretical semantics. We contribute to a unified framework by showing how the type/proof theoretical Edinburgh Logical Framework (LF) can be applied to the representation of model theoretical logics.We give a comprehensive formal representation of first-order logic, covering both its proof and its model theoretical semantics as well as its soundness in LF. For the model theory, we have to represent the mathematical foundation itself in LF, and we provide two solutions for that. Firstly, we give a meta-language that is strong enough to represent the model theory while being simple enough to be treated as a fragment of untyped set theory. Secondly, we represent Zermelo-Fraenkel set theory and show how it subsumes our meta-language. Specific models are represented as LF morphisms.All representations are given in and mechanically verified by the Twelf implementation of LF. Moreover, we use the Twelf module system to treat all connectives and quantifiers independently. Thus, individual connectives are available for reuse when representing other logics, and we obtain the first version of a feature library from which logics can be pieced together.Our results and methods are not restricted to first-order logic and scale to a wide variety of logical systems, thus demonstrating the feasibility of comprehensively formalizing large scale representation theorems in a logical framework.     

A case study in class library verification: Java’s vector class

This paper presents a verification of an invariant property for the Vector class from JAVA’s standard library (API). The property says (essentially) that the actual size of a vector is less than or equal to its capacity. It is shown that this “safety” or “data integrity” property is maintained by all methods of the Vector class, and that it holds for all objects created by the constructors of the Vector class. The verification of the Vector class invariant is done with the proof tool PVS. It is based on a semantics of JAVA in higher order logic. The latter is incorporated in a special purpose compiler, the LOOP tool, which translates JAVA classes into logical theories. It has been applied to the Vector class for this case study. The actual verification takes into account the object-oriented character of JAVA: (non-final) methods may always be overridden, so that one cannot rely on a particular implementation. Instead, one has to reason from method specifications in such cases. This project demonstrates the feasibility of tool-assisted verification of non-trivial properties for non-trivial JAVA classes. Published online: 10 May 2001     

A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs

This paper is concerned with a proof-theoretic observation about two kinds of proof systems for regular cyclic objects. It is presented for the case of two formal systems that are complete with respect to the notion of “recursive type equality” on a restricted class of recursive types in μ-term notation. Here we show the existence of an immediate duality with a geometrical visualization between proofs in a variant of the coinductive axiom system due to Brandt and Henglein and “consistency-unfoldings” in a variant of a 'syntactic-matching' proof system for testing equations between recursive types due to Ariola and Klop.Finally we sketch an analogous result of a duality between a similar pair of proof systems for bisimulation equivalence on equational specifications of cyclic term graphs.     

Syntactic Type Soundness Results for the Region Calculus

The region calculus of Tofte and Talpin is a polymorphically typed lambda calculus with annotations that make memory allocation and deallocation explicit. It is intended as an intermediate language for implementing Hindley-Milner typed functional languages such as ML without traditional trace-based garbage collection. Static region and effect inference can be used to annotate a statically typed ML program with memory management primitives. Soundness of the calculus with respect to the region and effect system is crucial to guarantee safe deallocation of regions, i.e., deallocation should only take place for objects which are provably dead. The original soundness proof by Tofte and Talpin requires a complex co-inductive safety relation. In this paper, we present two small-step operational semantics for the region calculus and prove their type soundness with respect to the region and effect system. Following the standard syntactic approach of Wright, Felleisen, and Harper, we obtain simple inductive proofs. The first semantics is store-less. It is simple and elegant and gives rise to perspicuous proofs. The second semantics provides a store-based model for the region calculus. Albeit slightly more complicated, its additional expressiveness allows us to model operations on references with destructive update. A pure fragment of both small-step semantics is then proven equivalent to the original big-step operational approach of Tofte and Talpin. This leads to an alternative soundness proof for their evaluation-style formulation.     

Modularity and expressibility for nets of relations

Modularity reflects the Frege Principle: any two expressions and which have the same meaning (semantics) can be replaced by each other in every appropriate context without changing the meaning of the overall expression. In [18] we identified observable relations and nets of observable relations as appropriate tools for the investigation of dataflow networks over nondeterministic agents. The observable relations are the Input-Output behaviors of (in general nondeterministic) dataflow agents. Moreover, the semantics of nets of observable relations is consistent with the input-output behavior of dataflow agents. In [18, 19] we showed that the main source of the Brock-Ackerman anomaly [2] is in the semantics of nets of relations. But it turns out that this semantics is not modular. The central objective of this paper is the characterization of modular classes of relations and hence indirectly the set of dataflow nets without anomalies. Another major theme which plays a technical role in this characterization, but is interesting in its own, is the expressibility for relational nets. The investigation also reveals the interesting role played by stable functions introduced by Berry [3]. Received: 11 December 1995 / 4 March 1997     

Aspects preserving properties

Aspect Oriented Programming can arbitrarily distort the semantics of programs. In particular, weaving can invalidate crucial safety and liveness properties of the base program. In this article, we identify categories of aspects that preserve some classes of properties. Specialized aspect languages are then designed to ensure that aspects belong to a specific category and, therefore, that woven programs will preserve the corresponding properties.Our categories of aspects, inspired by Katz’s, comprise observers, aborters, confiners and weak intruders. Observers introduce new instructions and a new local state but they do not modify the base program’s state and control-flow. Aborters are observers which may also abort executions. Confiners only ensure that executions remain in the reachable states of the base program. Weak intruders are confiners between two advice executions. These categories (along with two others) are defined formally based on a language independent abstract semantics framework. The classes of preserved properties are defined as subsets of LTL for deterministic programs and CTL* for non-deterministic ones. We can formally prove that, for any program, the weaving of any aspect in a category preserves any property in the related class.We present, for most aspect categories, a specialized aspect language which ensures that any aspect written in that language belongs to the corresponding category. It can be proved that these languages preserve the corresponding classes of properties by construction. The aspect languages share the same expressive pointcut language and are designed w.r.t. a common imperative base language.Each category and language is illustrated by simple examples. The appendix provides semantics and two instances of proofs: the proof of preservation of properties by a category and the proof that all aspects written in a language belong to the corresponding category.     

Polytime model checking for timed probabilistic computation tree logic

We consider the model checking problem for Timed Probabilistic Computation Tree Logic (TPCTL) introduced by H.A. Hansson and D. Jonsson, and studied in a recent book by H.A. Hansson [Han94]. The semantics of TPCTL is defined in terms of probabilistic transition systems. It is shown in [Han94] that model checking for TPCTL has exponential time complexity, the latter being measured in terms of the size of formula, the size of transition system and the value of explicit time that appears in the formula. Besides that, [Han94] describes some polytime decidable classes, the proofs being rather voluminous. We show, by a short proof, that this model checking problem is polytime decidable in the general case. The proof is essentially based on results on the complexity of Markov decision processes. Received: 2 May 1996 / 5 January 1998     

Combining Deep and Shallow Embeddings

This paper presents an approach for verifying translator correctness when the source language has formal semantics. Instead of verifying the translator implementation, a novel language mechanization combination is devised to reduce total complexity involved. A deep embedding is defined to serve as a baseline for specification meaning. For each specification, an equivalence proof is constructed and conducted to ensure that the translated shallow representation is semantically equivalent to the deep representation. Structure of an equivalence proof is systematic and can be derived from specification structure mechanically. The use of two embeddings also affects the embeddings favourably by enabling them to be defined in a simpler manner.     

Three-valued completion for abductive logic programs

In this paper, we propose a three-valued completion semantics for abductive logic programs, which solves some problems associated with the Console et al. two-valued completion semantics. The semantics is a generalization of Kunen's completion semantics for general logic programs, which is known to correspond very well to a class of effective proof procedures for general logic programs. Secondly, we propose a proof procedure for abductive logic programs, which is a generalization of a proof procedure for general logic programs based on constructive negation. This proof procedure is sound and complete with respect to the proposed semantics. By generalizing a number of results on general logic programs to the class of abductive logic programs, we present further evidence for the idea that limited forms of abduction can be added quite naturally to general logic programs.