Fundamenta Informaticae - Volume 33, issue 4

Authors: Hindley, Roger

Article Type: Other

DOI: 10.3233/FI-1998-33405

Citation: Fundamenta Informaticae, vol. 33, no. 4, pp. i-i, 1998

Authors: Brandt, Michael | Henglein, Fritz

Article Type: Research Article

Abstract: We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via simulation and bisimulation, respectively. The main novelty of the axiomatization is the fixpoint rule (or coinduction principle). It states that from A,P $\vdash$ P one may deduce A $\vdash$ P, where P is either a type equality τ = τ' or type containment τ ≤ τ' and the proof of the premise must be contractive in a sense we define …in this paper. In particular, a proof of A, P $\vdash$ P using the assumption axiom is not contractive. The fixpoint rule embodies a finitary coinduction principle and thus allows us to capture a coinductive relation in the fundamentally inductive framework of inference systems. The new axiomatizations are more concise than previous axiomatizations, particularly so for type containment since no separate axiomatization of type equality is required, as in Amadio and Cardelli's axiomatization. They give rise to a natural operational interpretation of proofs as coercions. In particular, the fixpoint rule corresponds to definition by recursion. Finally, the axiomatization is closely related to (known) efficient algorithms for deciding type equality and type containment. These can be modified to not only decide type equality and type containment, but also construct proofs in our axiomatizations efficiently. In connection with the operational interpretation of proofs as coercions this gives efficient (O(n2 ) time) algorithms for constructing efficient coercions from a type to any of its supertypes or isomorphic types. More generally, we show how adding the fixpoint rule makes it possible to characterize inductively a set that is coinductively defined as the kernel (greatest fixed point) of an inference system. Show more

Keywords: subtyping, type equality, recursive type, coercion, coinduction, operational interpretation, axiomatization, inference system, inference rule, fixpoint

DOI: 10.3233/FI-1998-33401

Citation: Fundamenta Informaticae, vol. 33, no. 4, pp. 309-338, 1998

Authors: Braüner, Torben

Article Type: Research Article

Abstract: Usually types of PCF are interpreted as cpos and terms as continuous functions. It is then the case that non-termination of a closed term of ground type corresponds to the interpretation being bottom; we say that the semantics is adequate. We shall here present an axiomatic approach to adequacy for PCF in the sense that we will introduce categorical axioms enabling an adequate semantics to be given. We assume the presence of certain “undefined” maps with the role of being the interpretation of non-terminating terms, but the order-structure is left out. This is different from previous approaches where some kind …of order-theoretic structure has been considered as part of an adequate categorical model for PCF. We take the point of view that partiality is the fundamental notion from which order-structure should be derived, which is corroborated by the observation that our categorical model induces an order-theoretic model for PCF in a canonical way. Show more

Keywords: Adequacy, PCF, categorical model

DOI: 10.3233/FI-1998-33402

Citation: Fundamenta Informaticae, vol. 33, no. 4, pp. 339-368, 1998

Authors: Stark, Ian

Article Type: Research Article

Abstract: The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state in the form of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between names and functions, the language can capture notions of scope, visibility and sharing. Originally motivated by the study of references in Standard ML, the nu-calculus has connections to local declarations in general; to the mobile processes of the π-calculus; and to security protocols in the spi-calculus. This paper introduces a logic of equations and relations which allows one to reason about expressions of the …nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs of contextual equivalence (also known as observational, or observable, equivalence). The logic is based on earlier operational techniques, providing the same power but in a much more accessible form. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names. Show more

Keywords: Names, nu-calculus, generativity, contextual equivalence, equational reasoning, operational reasoning, logical relations

DOI: 10.3233/FI-1998-33403

Citation: Fundamenta Informaticae, vol. 33, no. 4, pp. 369-396, 1998

Authors: Takeuti, Izumi

Article Type: Research Article

Abstract: Plotkin and Abadi have proposed a syntactic system for parametricity based on a second order predicate logic. This paper shows three theorems about that system. The first is consistency of the system, which is proved by the method of relativization. The second is that polyadic parametricities of recursive types are equivalent to each other. The third is that the theory of parametricity for recursive types is self-realizable. As a corollary of the third theorem, the theory of parametricity for recursive types satisfies the term extraction property.

Keywords: parametricity, polymorphism, typed lambda calculus

DOI: 10.3233/FI-1998-33404

Citation: Fundamenta Informaticae, vol. 33, no. 4, pp. 397-432, 1998