On specifications,subset types and interpretation of proposition in type theory

In this paper we discuss some practical aspects of using type theory as a programming and specification language, where the viewpoint is to use it not only as a basis for program synthesis but also as a programming language with a programming logic allowing us to do ordinary verification.The subset type has been added to type theory in order to avoid irrelevant information in programs. We give an example of a proof which illustrates the problems that may occur if the subset type is used in specifications when we have the standard interpretation of propositions as types. Harrop-formulas and Squash are then discussed as solutions to these problems. It is argued that they are not acceptable from a practical point of view.An extension of the theory to include the two new judgment forms:A is a proposition, andA is true, is then given and explained in terms of the old theory. The logical constants are no longer identified with the corresponding type theoretical constants, but propositions are interpreted as Gödel formulas, which allow us to introduce and justify logical rules similar to rules for classical logic. The interpretation is extended to include predicates defined by using reflections of the ordinary definition of Gödel formulas in a type of small propositions.The programming example is then revisited and stronger elimination rules are discussed.     

Remarks on Martin-Löf's partial type theory

In this paper we discuss Martin-Löf's partial type theory, that is type theory with general recursion, and in particular the consequences of the presence of a fixed point operator. We model Martin-Löf's logical framework domain-theoretically in the category of conditional upper semi lattices and parametrizations thereof. An interpretation of a type of sets in the logical framework, which defines partial type theory with one universe, is finally described.During the preparation of this paper, the first author was supported by the Swedish Natural Science Research Council as a PhD-student in mathematical logic.     

Non-differentiable variational principles

We develop a calculus of variations for functionals which are defined on a set of non-differentiable curves. We first extend the classical differential calculus in a quantum calculus, which allows us to define a complex operator, called the scale derivative, which is the non-differentiable analogue of the classical derivative. We then define the notion of extremals for our functionals and obtain a characterization in term of a generalized Euler-Lagrange equation. We finally prove that solutions of the Schrödinger equation can be obtained as extremals of a non-differentiable variational principle, leading to an extended Hamilton's principle of least action for quantum mechanics. We compare this approach with the scale relativity theory of Nottale, which assumes a fractal structure of space-time.     

How to assign ordinal numbers to combinatory terms with polymorphic types

The article investigates a system of polymorphically typed combinatory logic which is equivalent to G?del’s T. A notion of (strong) reduction is defined over terms of this system and it is proved that the class of well-formed terms is closed under both bracket abstraction and reduction. The main new result is that the number of contractions needed to reduce a term to normal form is computed by an ε ₀-recursive function. The ordinal assignments used to obtain this result are also used to prove that the system under consideration is indeed equivalent to G?del’s T. It is hoped that the methods used here can be extended so as to obtain similar results for stronger systems of polymorphically typed combinatory terms. An interesting corollary of such results is that they yield ordinally informative proofs of normalizability for sub-systems of second-order intuitionist logic, in natural deduction style.     

Generating a random cyclic permutation

We prove correct an algorithm that, givenn>0, stores in arrayb[0..n–1] a random cyclic permutation of the integers in 0..n–1, with each cyclic permutation having equal probability of being stored inb. The algorithm was developed by Sattolo; our contribution is to present a more convincing proof using standard program-proving methods.Dedicated to Peter Naur on the occasion of his 60th birthdayThis research was supported by the NSF under grant DCR-8320274.Visiting Cornell from the Computer Science Department, Jiangxi Normal University, Nanchang, People's Republic of China.     

Minimizing the number of transitions with respect to observation equivalence

Labeled transition systems (lts) provide an operational semantics for many specification languages. In order to abstract unrelevant details of lts's, manybehavioural equivalences have been defined; here observation equivalence is considered. We are interested in the following problem:Given a finite lts, which is the minimal observation equivalent lts corresponding to it? It is well known that the number of states of an lts can be minimized by applying arelational coarsest partition algorithm. However, the obtained lts is not unique (up to the renaming of the states): for an lts there may exist several observation equivalent lts's which have the minimal number of states but varying number of transitions. In this paper we show how the number of transitions can be minimized, obtaining a unique lts.     

Partial correctness of exits from concurrent structures

A rudimentary exit-mechanism from the parallel command of the language fragment CSP is introduced. A method for embedding invariants in a standard partial correctness system with pre-and postconditions is presented. Proof rules for exits from concurrent systems are introduced, and a simple data flow system is verified.     

带三次项的非线性四阶Schrdinger方程的一个局部能量守恒格式

本文构造了带三次项的非线性四阶Schodinger方程的一个局部能量守恒格式.证明了该格式是线性稳定的,且能保持离散的整体能量守恒律及离散的电荷守恒律.最后通过数值算例验证了理论结果的正确性.     

Prographes sylvestres et groupes profinis presque libres

In this article we want to give an analogous in the profinite case to the following theorem: an abstract group is free if and only if it acts freely on a tree. In a first time we define a combinatory object, the protrees, which are particular inductive systems extracted from projective systems of graphs. Then we define a notion of profinite action. These objects allow us to give the following analogous: a profinite group contains a dense abstract free subgroup if and only if it acts profreely on a protree.     

Formal power series with cyclically ordered exponents

We define and study a notion of ring of formal power series with exponents in a cyclically ordered group. Such a ring is a quotient of various subrings of classical formal power series rings. It carries a two variable valuation function. In the particular case where the cyclically ordered group is actually totally ordered, our notion of formal power series is equivalent to the classical one in a language enriched with a predicate interpreted by the set of all monomials.Received: 24 February 2003     

Partial inductive definitions as type-systems for λ-terms

To every partial inductive definitionD, a natural deduction calculusND(D) is associated. Not every such system will have the normalization property; specifically, there are definitionsD for whichND(D) permits non-normalizable deductions. A lambda calculus is formulated where the terms are used as objects realizing deductions inND(D), and is shown to have the Church-Rosser property. SinceND(D) permits non-normalizable deductions, there will be typed terms which are non-normalizable. It will, for example, be possible to obtain a typed fixed-point operator.     

Terminating general recursion

In Martin-Löf's type theory, general recursion is not available. The only iterating constructs are primitive recursion over natural numbers and other inductive sets. The paper describes a way to allow a general recursion operator in type theory (extended with propositions). A proof rule for the new operator is presented. The addition of the new operator will not destroy the property that all well-typed programs terminate. An advantage of the new program construct is that it is possible to separate the termination proof of the program from the proof of other properties.Dedicated to Peter Naur on the occasion of his 60:th birthday.     

Polytime,combinatory logic and positive safe induction

 We characterize the polynomial time operations as those which are provably total in a first order system, which comprises (untyped) combinatory logic with extensionality, together with positive “safe induction” on the set of binary strings. The formalization of safe induction is inspired by Leivants idea of ramification. We also show how to replace ramification by means of modal logic. Received: 14 June 2000 / Published online: 20 December 2001     

Expanding topological space,study and applications

In this paper, we introduce the notion of expanding topological space. We define the topological expansion of a topological space via local multi-homeomorphism over coproduct topology, and we prove that the coproduct family associated to any fractal family of topological spaces is expanding. In particular, we prove that the more a topological space expands, the finer the topology of its indexed states is. Using multi-homeomorphisms over associated coproduct topological spaces, we define a locally expandable topological space and we prove that a locally expandable topological space has a topological expansion. Specifically, we prove that the fractal manifold is locally expandable and has a topological expansion.     

Qregularity and an extension of the Evans-Griffiths criterion to vector bundles on quadrics

Here we define the concept of Qregularity for coherent sheaves on a smooth quadric hypersurface Q_n⊂Pⁿ⁺¹. In this setting we prove analogs of some classical properties. We compare the Qregularity of coherent sheaves on Q_n with the Castelnuovo-Mumford regularity of their extension by zero in Pⁿ⁺¹. We also classify the coherent sheaves with Qregularity −∞. We use our notion of Qregularity in order to prove an extension of the Evans-Griffiths criterion to vector bundles on quadrics. In particular, we get a new and simple proof of Knörrer’s characterization of ACM bundles.     

Algorithms for computing multiplier ideals

We give algorithms for computing multiplier ideals using Gröbner bases in Weyl algebras. To this end, we define a modification of Budur-Musta?aˇ-Saito’s generalized Bernstein-Sato polynomial. We present several examples computed by our algorithm.     

Bounds on the size of branch-and-bound proofs for integer knapsacks

Using a direct counting argument, we derive lower and upper bounds for the number of nodes enumerated by linear programming-based branch-and-bound (B&B) method to prove the integer infeasibility of a knapsack. We prove by example that the size of the B&B tree could be exponential in the worst case.     

A note on the height of thekth element in a heap

De Graaf and Kosters have studied the expected height of thekth element in a heap. They conjecture that, for largek, this is asymptotic to log₂ k + 0.72 .... We show that the height of thekth element is related to the depth of insertion in a digital search tree, and use this relation to prove their conjecture.This research was supported by grant FONDECYT (Chile) 91-1252.     

Maximum weight independent set in trees

Computing a maximum independent set, weighted or unweighted, isNP-hard for general as well as planar graphs. However, polynomial time algorithms do exist for solving this problem on special classes of graphs. In this paper we present an efficient algorithm for computing a maximum weight independent set in trees. A divide and conquer approach based on centroid decomposition of trees is used to compute a maximum weight independent set withinO(n logn) time, wheren is the number of vertices in the tree. We introduce a notion of analternating tree which is crucial in obtaining a new independent set from the previous one.