Typed operational semantics for higher-order subtyping

Bounded operator abstraction is a language construct relevant to object oriented programming languages and to ML2000, the successor to Standard ML. In this paper, we introduce , a variant of F_<:^ω with this feature and with Cardelli and Wegner’s kernel Fun rule for quantifiers. We define a typed-operational semantics with subtyping and prove that it is equivalent with , using logical relations to prove soundness. The typed-operational semantics provides a powerful and uniform technique to study metatheoretic properties of , such as Church–Rosser, subject reduction, the admissibility of structural rules, and the equivalence with the algorithmic presentation of the system that performs weak-head reductions.Furthermore, we can show decidability of subtyping using the typed-operational semantics and its equivalence with the usual presentation. Hence, this paper demonstrates for the first time that logical relations can be used to show decidability of subtyping.     

Basic Theory of F-Bounded Quantification

System F-bounded is a second-order typed lambda calculus, where the basic features of object-oriented languages can be naturally modelled. F-bounded extends the better known system F, in a way that provides an immediate solution for the treatment of the so-called “binary methods.” Although more powerful than F and also quite natural, system F-bounded has only been superficially studied from a foundational perspective and many of its essential properties have been conjectured but never proved in the literature. The aim of this paper is to give a solid foundation to F-bounded, by addressing and proving the key properties of the system. In particular, transitivity elimination, completeness of the type checking semi-algorithm, the subject reduction property for βη reduction, conservativity with respect to system F, and antisymmetry of a “full” subsystem are considered, and various possible formulations for system F-bounded are compared. Finally, a semantic interpretation of system F-bounded is presented, based on partial equivalence relations.     

A Representation of Fω in LF

We study how the type theory F_ω can be adequately represented in the meta-logical framework Twelf [16]. This development puts special emphasis on the way how terms, types, and kinds are represented in that it uses higher-order abstract syntax to model variable binding and dependent types to model typing constraints. Furthermore our design ensures that only well-typed terms and well-kinded types can be constructed. A possible application of this work lies in the development of safe intermediate languages for compilation.     

Efficient Inference of Object Types

M. Abadi and L. Cardelli have recently investigated a calculus of objects (1994). The calculus supports a key feature of object-oriented languages: an object can be emulated by another object that has more refined methods. Abadi and Cardelli presented four first-order type systems for the calculus. The simplest one is based on finite types and no subtyping, and the most powerful one has both recursive types and subtyping. Open until now is the question of type inference, and in the presence of subtyping "the absence of minimum typings poses practical problems for type inference." In this paper, we give an O(n³) algorithm for each of the four type inference problems and we prove that all the problems are P-complete. We also indicate how to modify the algorithms to handle functions and records.     

Algebraic Riccati equation and J-spectral factorization for estimation

In this paper we investigate on the existence of the stabilizing solution of the algebraic Riccati equation (ARE) related to the filtering problem with a prescribed attenuation level γ. It is well known that such a solution exists and is positive definite for γ larger than a certain γ_F and it does not exist for γ smaller than a certain γ₀. We consider the intermediate case γ(γ₀,γ_F] and show that in this interval the stabilizing solution does exist, except for a finite number of values of γ. We show how the solution of the ARE may be employed to obtain a minimum-phase J-spectral factor of the J-spectrum associated with the filtering problem.     

Homomorphic characterizations of recursively enumerable languages with very small language classes

In this paper, we attempt to characterize the class of recursively enumerable languages with much smaller language classes than that of linear languages. Language classes, and , of (i,j) linear languages and (i,j) minimal linear languages are defined by posing restrictions on the form of production rules and the number of nonterminals. Then the homomorphic characterizations of the class of recursively enumerable languages are obtained using these classes and a class, , of minimal linear languages. That is, for any recursively enumerable language L over Σ, an alphabet Δ, a homomorphism h : Δ^*→Σ^* and two languages L₁ and L₂ over Δ in some classes mentioned above can be found such that L = h(L₁∩L₂). The membership relations of L₁ and L₂ of the main results are as follows:(I) For posing restrictions on the forms of production rules, the following result is obtained:(1) and .This result is the best one and cannot be improved using . However, with posing more restriction on L₂, this result can be improved and the follwing statement is obtained.(2) and .(II) For posing restrictions on the numbers of nonterminals, the follwing result is obtained.(3) and .We believe this result is also the best.     

A categorical framework for typing CCS-style process communication

Category theory has proved a useful tool in the study of type systems for sequential programming languages. Various approaches have been proposed to use categorical models to examine the type structures appropriate to concurrent systems. In this paper, we outline some of these approaches, such as interaction categories, and argue that they are not appropriate to model the handshake communication mechanism as used e.g. in CCS or the π-calculus. We propose an alternative general categorical framework for examining the type structure of such systems, and exhibit its categorical structure, which is similar to that of existing approaches. We then examine in detail an instance of this framework, based on a simple fragment of CCS. We prove that it is isomorphic to a syntactic category constructed from a process algebra similar to CCS, with a fusion operator, as in the fusion calculus. Thus, we make explicit some of the type structure implicitly present in such a process algebra.     

Infinitary Logic and Inductive Definability over Finite Structures

The extensions of first-order logic with a least fixed point operator (FO + LFP) and with a partial fixed point operator (FO + PFP) are known to capture the complexity classes P and PSPACE respectively in the presence of an ordering relation over finite structures. Recently, Abiteboul and Vianu (in "Proceedings of the 23rd ACM Symposium on the Theory of Computing," 1991) investigated the relationship of these two logics in the absence of an ordering, using a machine model of generic computation. In particular, they showed that the two languages have equivalent expressive power if and only if P = PSPACE. These languages can also be seen as fragments of an infinitary logic where each formula has a bounded number of variables, L^ω_∞ω, (see, for instance, Kolaitis and Vardi, in "Proceedings of the 5th IEEE Symposium on Logic in Computer Science," pp. 156-167, 1990). We investigate this logic on finite structures and provide a normal form for it. We also present a treatment of Abiteboul and Vianu′s results from this point of view. In particular, we show that we can write a formula of FO + LFP that defines an ordering of the L^k_∞ω, types uniformly over all finite structures. One consequence of this is a generalization of the equivalence of FO + LFP and P from ordered structures to classes of structures where every element is definable. We also settle a conjecture mentioned by Abiteboul and Vianu by showing that FO + LFP is properly contained in the polynomial time computable fragment of L^ω_∞ω, raising the question of whether the latter fragment is a recursively enumerable class.     

Infinitary logics and 0–1 laws

We investigate the infinitary logic L_∞ω^ω, in which sentences may have arbitrary disjunctions and conjunctions, but they involve only finite numbers of distinct variables. We show that various fixpoint logics can be viewed as fragments of L_∞ω^ω, and we describe a game-theoretic characterization of the expressive power of the logic. Finally, we study asymptotic probabilities of properties expressible in L_∞ω^ω on finite structures. We show that the 0–1 law holds for L_∞ω^ω, i.e., the asymptotic probability of every sentence in this logic exists and is equal to either 0 or 1. This result subsumes earlier work on asymptotic probabilities for various fixpoint logics and reveals the boundary of 0–1 laws for infinitary logics.     

Projective Linear Groups as Galois Groups overQvia Modular Representations

We give an algorithm for the determination of the finitely many primes such that the image of the modular Galois representations attached to a weight 2 newform on Γ₀(N) without complex multiplication or inner twists may not be “as large as possible". We apply the algorithm to suitable newforms and we obtain the realization of the groups PSL(2,F_ℓ²),PGL (2,F_ℓ³) andPSL (2,F_ℓ⁴) as Galois groups overQfor high density sets of primes.     

On the Power of Multiple Reads in a Chip

A chip algorithm is called r-multilective if it reads its input bits r times. In this paper we relate the r-bound communication complexity of a language L and the area requirement for an r-multilective chip algorithm of a related language . More specifically Improving known lower bounds on the r-bound communication complexity of certain languages, we obtain several hierarchies of r-multilective languages depending on the parameter r. For example, if 0 < r < s, then there are constants 0 < c, c′ such that for infinitely many n there is a language L_n {0, 1}ⁿ such that there is an s-multilective algorithm recognizing L_n using area at most c log n and any r-multilective algoerithm recognizing L_n requires area at least c′n/log n. Similar results have been known only for s = 2 and r = 1 and have been open in other cases.     

Languages Defined with Modular Counting Quantifiers

We prove that a regular language defined by a boolean combination of generalized Σ₁-sentences built using modular counting quantifiers can be defined by a boolean combination of Σ₁-sentences in which only regular numerical predicates appear. The same statement, with “Σ₁” replaced by “first-order,” is equivalent to the conjecture that the nonuniform circuit complexity class ACC is strictly contained in NC¹. The argument introduces some new techniques, based on a combination of semigroup theory and Ramsey theory, which may shed some light on the general case.     

Type Destructors

We study a variant of System F_≤ that integrates and generalizes several existing proposals for calculi with “structural typing rules.” To the usual type constructors (→, ×, All, Some, Rec) we add a number of type destructors, each internalizing a useful fact about the subtyping relation. For example, in F_≤ with products every closed subtype of a product S×T must itself be a product S′×T′ with S′<:S and T′<:T. We internalise this observation by introducing type destructors .1 and .2 and postulating an equivalence T=_ηT.1×T.2 whenever T<:U×V (including, for example, when T is a variable). In other words, every subtype of a product type literally is a product type, modulo η-conversion. Adding type destructors provides a clean solution to the problem of polymorphic update without introducing new term formers, new forms of polymorphism, or quantification over type operators. We illustrate this by giving elementary presentations of two well-known encodings of objects, one based on recursive record types and the other based on existential packages. The formulation of type destructors poses some tricky meta-theoretic problems. We discuss two different variants: an “ideal” system where both constructors and destructors appear in general forms, and a more modest system, F_≤^TD, which imposes some restrictions in order to achieve a tractable metatheory. The properties of the latter system are developed in detail.     

Type Theory and Language Constructs for Objects with States

In current class-based Object-Oriented Programming Languages (OOPLs), object types include only static features. How to add object dynamic behaviors modeled by Harel's statecharts into object types is a challenging task. We propose adding states and state transitions, which are largely unstated in object type theory, into object type definitions and typing rules. We argue that dynamic behaviors of objects should be part of object type definitions. We propose our type theory, the τ-calculus, which refines Abadi and Cardelli's ζ-calculus, in modeling objects with their dynamic behaviors. In our proposed type theory, we also explain that a subtyping relation between object types should imply the inclusion of their dynamic behaviors. By adding states and state transitions into object types, we propose modifying programming language constructs for state tracking.     

A Proof of Strong Normalization for F2, Fω, and Beyond

We present an evaluation technique for proving strong normalization (SN). We use the technique to give SN proofs for F₂, F-bounded quantification, subtypes, and Fω. The evaluation technique derives SN as a corollary of the soundness of the typing rules under an appropriate evaluation semantics. The evaluation semantics yields simpler type sets than those used in the earlier SN proofs. The type sets discussed here form a complete lattice under classical union and intersection. The simplified type sets allow a simplified treatment of a variety of type constructors.     

Equational Formulas with Membership Constraints

We propose a set of transformation rules for first order formulae whose atoms are either equations between terms or "membership constraints" tζ. ζ can be interpreted as a regular tree language (ζ is called a sort in the algebraic specification community) or as a tree language in any class of languages which satisfies some adequate closure and decidability properties. This set of rules is proved to be correct, terminating, and complete. This provides a quantifier elimination procedure: for every regular tree language , the first order theory of some structure defining is decidable. This extends the results of several previously published results. We also show how to apply our results to automatic inductive proofs in equational theories.     

On non context-free grammar forms

A grammar formF defines via a so-calledinterpretation mechanism, a family of languages(F). In this paper we establish that for many grammar formsF, (the family of context-free languages) implies(F)= _RE (the family of recursively enumerable sets). We conjecture that this is also true in general. Because of this, it seems necessary to use restricted interpretations for non context-free grammar forms, a form giving then rise to a family We compare the obvious alternatives for restricting interpretations and focus attention on two promising alternatives, _Q (_F) and _st(F) and their combination _{Q, st}(F). Using st-interpretations, surprising families can be generated and strong normal form results can be obtained. Closure results and decidability results are also given. UnderQ, st-interpretation, it is possible to characterize a number of well-known families of languages between _CF and _RE, including the families of EOL, ETOL, matrix and scattered context languages.Part of this work was carried out while the third and fourth authors were visiting the University of Karlsruhe. Part of this work was supported by the Natural Sciences and Engineering Research Council of Canada Grant No. A-7700.     

Integration of parametric and “ad hoc” second order polymorphism in a calculus with subtyping

In this paper we define an extension ofF [CUG92] to which we add functions that dispatch on different terms according to the type they receive as argument. In other words, we enrich the explicit parametric polymorphism ofF by an explicit ad hoc polymorphism (according the classification of [Str67]). We prove that the calculus we obtain, calledF ^& , enjoys the properties of Church-Rosser and Subject Reduction and that its proof system is coherent. We also define a significant subcalculus for which the subtyping is decidable. This extension has not only a logical interest but it is strongly motivated by the foundation of a broadly used programming style: object-oriented programming. The connections betweenF ^& and object-oriented languages are widely stressed, and the modelling byF ^& of some features of the object-oriented style is described, continuing the work of [CGL96].Part of this work has appeared under the title F ^& : integrating parametric and ad hoc second order polymorphism in the 4th International Workshop on Database Programming Languages. New York City, August 1993.The author was supported by grant n. 203.01.56 of the Consiglio Nazionale delle Ricerche-Comitato Nazionale delle Scienze Matematiche to work at LIENS.     

Programmable Rewriting Strategies in Haskell: — White Paper —

Programmable rewriting strategies provide a valuable tool for implementing traversal functionality in grammar-driven (or schema-driven) tools. The working Haskell programmer has access to programmable rewriting strategies via two similar options: (i) the Strafunski bundle for generic functional programming and language processing, and (ii) the “Scrap Your Boilerplate” approach to generic functional programming. Basic rewrite steps are encoded as monomorphic functions on datatypes. Rewriting strategies are polymorphic functions composed from appropriate basic strategy combinators.We will briefly review programmable rewriting strategies in Haskell. We will address the following questions:

• What are the merits of Haskellish strategies?

• What is the relation between strategic programming and generic programming?

• What are the challenges for future work on functional strategies?

From Functional Programs to Interaction Nets via the Rewriting Calculus

We use the ρ-calculus as an intermediate language to compile functional languages with pattern-matching features, and give an interaction net encoding of the ρ-terms arising from the compilation. This encoding gives rise to new strategies of evaluation, where pattern-matching and 'traditional' β-reduction can proceed in parallel without overheads.