A Logic for Reasoning about Generic Judgments

This paper presents an extension of a proof system for encoding generic judgments, the logic FOλ^Δ of Miller and Tiu, with an induction principle. The logic FOλ^Δ is itself an extension of intuitionistic logic with fixed points and a “generic quantifier”, , which is used to reason about the dynamics of bindings in object systems encoded in the logic. A previous attempt to extend FOλ^Δ with an induction principle has been unsuccessful in modeling some behaviours of bindings in inductive specifications. It turns out that this problem can be solved by relaxing some restrictions on , in particular by adding the axiom B≡x.B, where x is not free in B. We show that by adopting the equivariance principle, the presentation of the extended logic can be much simplified. Cut-elimination for the extended logic is stated, and some applications in reasoning about an object logic and a simply typed λ-calculus are illustrated.     

Call-by-name, call-by-value and the λ-calculus

This paper examines the old question of the relationship between ISWIM and the λ-calculus, using the distinction between call-by-value and call-by-name. It is held that the relationship should be mediated by a standardisation theorem. Since this leads to difficulties, a new λ-calculus is introduced whose standardisation theorem gives a good correspondence with ISWIM as given by the SECD machine, but without the letrec feature. Next a call-by-name variant of ISWIM is introduced which is in an analogous correspondence withthe usual λ-calculus. The relation between call-by-value and call-by-name is then studied by giving simulations of each language by the other and interpretations of each calculus in the other. These are obtained as another application of the continuation technique. Some emphasis is placed throughout on the notion of operational equality (or contextual equality). If terms can be proved equal in a calculus they are operationally equal in the corresponding language. Unfortunately, operational equality is not preserved by either of the simulations.     

A formalised first-order confluence proof for the λ-calculus using one-sorted variable names

We present the titular proof development that has been verified in Isabelle/HOL. As a first, the proof is conducted exclusively by the primitive proof principles of the standard syntax and of the considered reduction relations: the naive way, so to speak. Curiously, the Barendregt Variable Convention takes on a central technical role in the proof. We also show: (i) that our presentation of the λ-calculus coincides with Curry’s and Hindley’s when terms are considered equal up to α-equivalence and (ii) that the confluence properties of all considered systems are equivalent.     

A semantic characterization of the well-typed formulae of λ-calculus

A model-theoretic operation is characterized that preserves the property of being a model of typed λ-calculus (i.e., the result of applying it to a model of typed λ-calculus is another model of typed λ-calculus). An expression is well-typed iff the class of its models is closed under this operation.     

Equational programming in λ-calculus via SL-systems. Part 1

A system of equations in the λ-calculus is a set of formulas of Λ (the equations) together with a finite set of variables of Λ (the unknowns). A system s is said to be β-solvable (βη-solvable) iff there exists a simultaneous substitution with closed λ-terms for the unknowns that makes the equations of s theorems in the theory β (βη). A system s can be viewed as a set of specifications (the equations) for a finite set of programs (the unknowns) whereas a solution for s yields executable codes for such programs.

A class of systems for which the solvability problem is effectively decidable defines an equational programming language and a system solving algorithm for defines a compiler for such language.

This leads us to consider separation-like systems (SL-systems), i.e. systems with equations having form , where x is an unknown and z is a free variable which is not an unknown.

We show that the β (βη)-solvability problem for SL-systems is undecidable.

On the other hand we are able to define a class of SL-systems (regular SL-systems) for which the β-solvability problem is decidable in Polynomial Time. Such class yields an equational programming language in which self-application is handled, constraints on executable code to be generated by the compiler can be specified by the user and (properties of) data structures can be described in an abstract way.     

Equational programming in λ-calculus via SL-systems. Part 2

A system of equations in the λ-calculus is a set of formulas of Λ (the equations) together with a finite set of variables of Λ (the unknowns). A system s is said to be β-solvable (βη-solvable) iff there exists a simultaneous substitution with closed λ-terms for the unknowns that makes the equations of s theorems in the theory β (βη). A system s can be viewed as a set of specifications (the equations) for a finite set of programs (the unknowns) whereas a solution for s yields executable codes for such programs.

A class of systems for which the solvability problem is effectively decidable defines an equational programming language and a system solving algorithm for defines a compiler for such language.

This leads us to consider separation-like systems (SL-systems), i.e. systems with equations having form , wherex is an unknown and z is a free variable which is not an unknown.

It is known that the β (βη)-solvability problem for SL-systems is undecidable.

Here we show that there is a class of SL-systems (NP-regular SL-systems) for which the β-solvability problem is NP-complete. Moreover, we show that any SL-system s can be transformed into an NP-regular SL-system s. This transformation consists of adding abstractions to the LHS occurrences of the RHS variables of s. In this sense NP-regular SL-systems isolate the source of undecidability for SL-systems, namely: a shortage of abstractions on the LHS occurrences of the RHS variables.

NP-regular SL-systems yield an equational programming language in which unrestrained self-application is handled, constraints on executable code to be generated by the compiler can be specified by the user and (properties of) data structures can be described in an abstract way. However, existence of executable code satisfying a specification in such language is an NP-complete problem. This is the price we have to pay for allowing unrestrained self-application in our language.     

Towards a proof theory of rewriting: the simply typed 2λ-calculus

This paper describes the simply typed 2λ-calculus, a language with three levels: types, terms and rewrites. The types and terms are those of the simply typed λ-calculus, and the rewrites are expressions denoting sequences of β-reductions and η-expansions. An equational theory is imposed on the rewrites, based on 2-categorical justifications, and the word problem for this theory is solved by finding a canonical expression in each equivalence class. The canonical form of rewrites allows us to prove several properties of the calculus, including a strong form of confluence and a classification of the long-βη-normal forms in terms of their rewrites. Finally we use these properties as the basic definitions of a theory of categorical rewriting, and find that the expected relationships between confluence, strong normalisation and normal forms hold.     

Can LCF be topped? Flat lattice models of typed λ-calculus

Plotkin ((1977) Theoret. Comput. Sci. 5: 223–256) examines the denotational semantics of PCF (essentially typed λ-calculus with arithmetic and looping). The standard Scott semantics V is computationally adequate but not fully abstract; with the addition of some parallel facilities, it becomes fully abstract, and with the addition of an existential operator, denotationally universal. We consider carrying out the same program for , the Scott models built from flat lattices rather than flat cpo's. Surprisingly, no computable extension of PCF can be denotationally universal; perfectly reasonable semantic values such as supremum and Plotkin's “parallel or” cannot be definable. There is an unenlightening fully abstract extension _A (approx), based on Gödel numbering and syntactic analysis. Unfortunately, this is the best we can do; operators defined by PCF-style rules cannot give a fully abstract language. (There is a natural and desirable property, operational extensionality, which prevents full abstraction with respect to .) However, we show that Plotkin's program can be carried out for a nonconfluent evaluator.     

Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts

We illustrate a methodology for formalizing and reasoning about Abadi and Cardelli’s object-based calculi, in (co)inductive type theory, such as the Calculus of (Co)Inductive Constructions, by taking advantage of natural deduction semantics and coinduction in combination with weak higher-order abstract syntax and the Theory of Contexts. Our methodology allows us to implement smoothly the calculi in the target metalanguage; moreover, it suggests novel presentations of the calculi themselves. In detail, we present a compact formalization of the syntax and semantics for the functional and the imperative variants of the ς-calculus. Our approach simplifies the proof of subject deduction theorems, which are proved formally in the proof assistant Coq with a relatively small overhead. Supported by UE project IST-CA-510996 Types and French grant CNRS ACI Modulogic.     

Strong normalisation in the π-calculus

We introduce a typed π-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed λ-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.     

On the Expressive Power of Polyadic Synchronisation in π-calculus

We extend the π-calculus with polyadic synchronisation, a generalisation of the communication mechanism which allows channel names to be composite. We show that this operator embeds nicely in the theory of π-calculus, and makes it possible to derive divergence-free encodings of distributed calculi. We give a separation result between the π-calculus with polyadic synchronisation (^eπ) and the original calculus, in the style of an analogous result given by Palamidessi for mixed choice. We encode Local Area π showing how to control the local use of resources in ^eπ.     

On the latent roots of λ matrices

In this paper we consider equations defined by (1.3)–(1.2)–(1.4). We describe in detail three algorithms for the approximate determination of |λ_nr|, for |λ₁| resp. for one of the λ_j's. The single steps of the algorithms are the four fundamental operations and the positive value of k^th roots of positive numbers and the main interest of them lies in the fact that (the algorithms themselves and so) their lengths depend only on n, r and the prescribed relative error and not on the entries of the matrices A_ν.     

On the decidability of fragments of the asynchronous π-calculus

We study the decidability of a reachability problem for various fragments of the asynchronous π-calculus. We consider the combination of three main features: name generation, name mobility, and unbounded control. We show that the combination of name generation with either name mobility or unbounded control leads to an undecidable fragment. On the other hand, we prove that name generation without name mobility and with bounded control is decidable by reduction to the coverability problem for Petri Nets.     

A Third-Order Representation of the λμ-Calculus

Higher-order logical frameworks provide a powerful technology to reason about object languages with binders. This will be demonstrated for the case of the λμ-calculus with two different binders which can most elegantly be represented using a third-order constant. Since cases of third- and higher-order encodings are very rare in comparison with those of second order, a second-order representation is given as well and equivalence to the third-order representation is proven formally.     

A syntactical proof of the operational equivalence of two λ-terms

In this paper we present a purely syntactical proof of the operational equivalence of I = λxx and the λ-term J that is the η-infinite expansion of I.     

Adaptive λ-tracking for a class of infinite-dimensional systems

For a class of high-gain stabilizable multivariable linear infinite-dimensional systems we present an adaptive control law which achieves approximate asymptotic tracking in the sense that the tracking error tends asymptotically to a ball centred at 0 and of arbitrary prescribed radius λ>0. This control strategy, called λ-tracking, combines proportional error feedback with a simple nonlinear adaptation of the feedback gain. It does not involve any parameter estimation algorithms, nor is it based on the internal model principle. The class of reference signals is W^1,∞, the Sobolev space of absolutely continuous functions which are bounded and have essentially bounded derivative. The control strategy is robust with respect to output measurement noise in W^1,∞ and bounded input disturbances. We apply our results to retarded systems and integrodifferential systems.     

Application of the λ-scheme to a chemically reacting supersonic jet flow

The λ-scheme is used as the basuc integration method to compute the inviscid, chemically reacting flow of a supersonic jet. To encounter the different time scales characteristic on the fluid and chemical processes, during the explicit integration of the time-dependent problem equations, the chemical source terms for species and energy are replaced by averaged integral values. With the definition of the averaged source terms, special regard iss given to the physical fact that chemical reactions occur simultaneously with the transport of the species along particle paths.     

Type-level Computation Using Narrowing in Ωmega

Ωmega is an experimental system that combines features of both a programming language and a logical reasoning system. Ωmega is a language with an infinite hierarchy of computational levels. Terms at one level are classified (or typed) by terms at the next higher level. In this paper we report on using two different computational mechanisms. At the value level, computation is performed by reduction, and is largely unconstrained. At all higher levels, computation is performed by narrowing.     

Godel系统中一类子代数上的广义重言式理论

将Godel辑系统中的广义重言式理论进行推广,讨论了一类无限子代数上的广义重言式理论,并利用可达广义重言式的概念在G的标准子代数E0中给出F（S）关于┑同余的一个分划。