Sound and complete models of contracts

2006 ◽  
Vol 16 (4-5) ◽  
pp. 375-414 ◽  
Author(s):  
MATTHIAS BLUME ◽  
DAVID McALLESTER
Keyword(s):  
Ad Hoc ◽  
Expressive Power ◽  
Higher Order ◽  
Original Version ◽  
Order Types ◽  
Restricted Form ◽  
Soundness And Completeness ◽  
Recursive Contracts ◽  
Intuitive Interpretation ◽  
Typed Languages

Even in statically typed languages it is useful to have certain invariants checked dynamically. Findler and Felleisen gave an algorithm for dynamically checking expressive higher-order types called contracts. They did not, however, give a semantics of contracts. The lack of a semantics makes it impossible to define and prove soundness and completeness of the checking algorithm. (Given a semantics, a sound checker never reports violations that do not exist under that semantics; a complete checker is – in principle – able to find violations when violations exist.) Ideally, a semantics should capture what programmers intuitively feel is the meaning of a contract or otherwise clearly point out where intuition does not match reality. In this paper we give an interpretation of contracts for which we prove the Findler-Felleisen algorithm sound and (under reasonable assumptions) complete. While our semantics mostly matches intuition, it also exposes a problem with predicate contracts where an arguably more intuitive interpretation than ours would render the checking algorithm unsound. In our semantics we have to make use of a notion of safety (which we define in the paper) to avoid unsoundness. We are able to eliminate the “leakage” of safety into the semantics by changing the language, replacing the original version of unrestricted predicate contracts with a restricted form. The corresponding loss in expressive power can be recovered by making safety explicit as a contract. This can be done either in ad-hoc fashion or by including general recursive contracts. The addition of recursive contracts has far-reaching implications, deeply affecting the formulation of our model and requiring different techniques for proving soundness.

scholarly journals Constructive natural deduction and its ‘ω-set’ interpretation

1991 ◽  
Vol 1 (2) ◽  
pp. 215-254 ◽  
Author(s):  
Giuseppe Longo ◽  
Eugenio Moggi
Keyword(s):  
Type Theory ◽  
Natural Deduction ◽  
Expressive Power ◽  
Higher Order ◽  
Second Order ◽  
Deduction Theorem ◽  
Natural Numbers ◽  
Experienced Reader ◽  
Order Types ◽  
The Universe

Various Theories of Types are introduced, by stressing the analogy ‘propositions-as-types’: from propositional to higher order types (and Logic). In accordance with this, proofs are described as terms of various calculi, in particular of polymorphic (second order) λ-calculus. A semantic explanation is then given by interpreting individual types and the collection of all types in two simple categories built out of the natural numbers (the modest sets and the universe of ω-sets). The first part of this paper (syntax) may be viewed as a short tutorial with a constructive understanding of the deduction theorem and some work on the expressive power of first and second order quantification. Also in the second part (semantics, §§6–7) the presentation is meant to be elementary, even though we introduce some new facts on types as quotient sets in order to interpret ‘explicit polymorphism’. (The experienced reader in Type Theory may directly go, at first reading, to §§6–8).

The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic

2021 ◽  
Vol 178 (1-2) ◽  
pp. 1-30
Author(s):  
Florian Bruse ◽  
Martin Lange ◽  
Etienne Lozes
Keyword(s):  
Model Checking ◽  
Lower Bounds ◽  
Expressive Power ◽  
Higher Order ◽  
Order Logic ◽  
High Complexity ◽  
Transition Systems ◽  
Recursive Formulas ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed λ-calculus into the modal μ-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most k < 0. In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in (k − 1)-EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.

scholarly journals The complexity of type inference for higher-order typed lambda calculi

1994 ◽  
Vol 4 (4) ◽  
pp. 435-477 ◽  
Author(s):  
Fritz Henglein ◽  
Harry G. Mairson
Keyword(s):  
Lower Bounds ◽  
Higher Order ◽  
Type Inference ◽  
Boolean Logic ◽  
Turing Machines ◽  
Technical Tool ◽  
Inference Problem ◽  
Exponential Time ◽  
First Order ◽  
Order Types

AbstractWe analyse the computational complexity of type inference for untyped λ-terms in the second-order polymorphic typed λ-calculus (F2) invented by Girard and Reynolds, as well as higher-order extensions F3, F4, …, Fω proposed by Girard. We prove that recognising the F2-typable terms requires exponential time, and for Fω the problem is non-elementary. We show as well a sequence of lower bounds on recognising the Fk-typable terms, where the bound for Fk+1 is exponentially larger than that for Fk.The lower bounds are based on generic simulation of Turing Machines, where computation is simulated at the expression and type level simultaneously. Non-accepting computations are mapped to non-normalising reduction sequences, and hence non-typable terms. The accepting computations are mapped to typable terms, where higher-order types encode reduction sequences, and first-order types encode the entire computation as a circuit, based on a unification simulation of Boolean logic. A primary technical tool in this reduction is the composition of polymorphic functions having different domains and ranges.These results are the first nontrivial lower bounds on type inference for the Girard/Reynolds system as well as its higher-order extensions. We hope that the analysis provides important combinatorial insights which will prove useful in the ultimate resolution of the complexity of the type inference problem.

Integration of Geometry Definition and Wave Analysis Software

2002 ◽  
Author(s):  
C.-H. Lee ◽  
J. S. Letcher ◽  
R. G. Mark ◽  
J. N. Newman ◽  
D. M. Shook ◽  
...  
Keyword(s):  
Ad Hoc ◽  
Substantial Reduction ◽  
Offshore Structures ◽  
Higher Order ◽  
Surface Patch ◽  
Surface Geometry ◽  
Hydrodynamic Analysis ◽  
Extra Effort ◽  
Wave Effects ◽  
Low Order

In a paper presented at OMA 2001, an extension of the panel code WAMIT was described where the surface geometry of the structure is represented explicitly and the solution for the velocity potential is approximated by higher-order B-splines. This permits an exact representation of the geometry in many applications, and avoids the effort and approximations inherent in preparing traditional low-order panel inputs. However the algorithms for the explicit geometry definition must be coded in special ad hoc subroutines for each type of structure. In the present paper we describe recent work to integrate the programs MultiSurf and WAMIT, in a manner which circumvents the need for special subroutines. In most practical cases this leads to a substantial reduction of the work required to perform computations of wave effects on structures. MultiSurf is a CAD program which enables users to define surface geometry with a high degree of accuracy, efficiency, and generality. It has been used extensively to develop low-order panel input files for ships and offshore structures, as well as for a variety of other marine design applications. The fundamental approach is to represent each part of the surface which is smooth and continuous by a parametric surface ‘patch’, using appropriate surface constructions which allow these patches to be joined robustly. The kernel of MultiSurf, known as RGKernel, includes the necessary code to evaluate surface locations and derivatives. A close integration of MultiSurf and WAMIT has been achieved by linking RGKernel with WAMIT, so that the same geometry can be reproduced during the hydrodynamic analysis. This integration makes it possible for users to define the geometry of structures interactively in MultiSurf, and to transfer this representation to WAMIT without significant extra effort. Thus the hydrodynamic analysis can be performed with exact or highly accurate representations of the geometry, and with the increased accuracy and efficiency inherent in the higher-order solution based on B-spline representation of the potential. After a brief explanation of the methodology, illustrative results are described for several examples. Comparisons are made of the accuracy, efficiency and workload, relative to the conventional use of low-order panels.

scholarly journals HOPLA--A Higher-Order Process Language

2002 ◽  
Vol 9 (49) ◽  
Author(s):  
Mikkel Nygaard ◽  
Glynn Winskel
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Expressive Power ◽  
Higher Order ◽  
Domain Theory ◽  
Order Process ◽  
Encode Process ◽  
Mobile Ambients ◽  
Computation Path ◽  
Congruence Properties

A small but powerful language for higher-order nondeterministic processes is introduced. Its roots in a linear domain theory for concurrency are sketched though for the most part it lends itself to a more operational account. The language can be viewed as an extension of the lambda calculus with a ``prefixed sum'', in which types express the form of computation path of which a process is capable. Its operational semantics, bisimulation, congruence properties and expressive power are explored; in particular, it is shown how it can directly encode process languages such as CCS, CCS with process passing, and mobile ambients with public names.

scholarly journals New-HOPLA--A Higher-Order Process Language with Name Generation

2004 ◽  
Vol 11 (21) ◽  
Author(s):  
Glynn Winskel ◽  
Francesco Zappa Nardelli
Keyword(s):  
Operational Semantics ◽  
Expressive Power ◽  
Higher Order ◽  
Domain Theory ◽  
Process Algebras ◽  
Order Process ◽  
Pi Calculus ◽  
Mobile Ambients ◽  
Congruence Properties

This paper introduces new-HOPLA, a concise but powerful language for higher-order nondeterministic processes with name generation. Its origins as a metalanguage for domain theory are sketched but for the most part the paper concentrates on its operational semantics. The language is typed, the type of a process describing the shape of the computation paths it can perform. Its transition semantics, bisimulation, congruence properties and expressive power are explored. Encodings are given of well-known process algebras, including pi-calculus, Higher-Order pi-calculus and Mobile Ambients.

scholarly journals On Higher-Order Probabilistic Subrecursion

2021 ◽  
Vol Volume 17, Issue 4 ◽  
Author(s):  
Flavien Breuvart ◽  
Ugo Dal Lago ◽  
Agathe Herrou
Keyword(s):  
Expressive Power ◽  
Higher Order ◽  
Probabilistic Choice ◽  
The Way

We study the expressive power of subrecursive probabilistic higher-order calculi. More specifically, we show that endowing a very expressive deterministic calculus like G\"odel's $\mathbb{T}$ with various forms of probabilistic choice operators may result in calculi which are not equivalent as for the class of distributions they give rise to, although they all guarantee almost-sure termination. Along the way, we introduce a probabilistic variation of the classic reducibility technique, and we prove that the simplest form of probabilistic choice leaves the expressive power of $\mathbb{T}$ essentially unaltered. The paper ends with some observations about the functional expressive power: expectedly, all the considered calculi capture the functions which $\mathbb{T}$ itself represents, at least when standard notions of observations are considered.

Sign in / Sign up

Export Citation Format

Share Document