Realisability semantics of parametric polymorphism, general references and recursive types

2010 ◽  
Vol 20 (4) ◽  
pp. 655-703 ◽  
Author(s):  
LARS BIRKEDAL ◽  
KRISTIAN STØVRING ◽  
JACOB THAMSBORG
Keyword(s):  
Metric Spaces ◽  
Logical Relation ◽  
Data Types ◽  
General Reference ◽  
New Approach ◽  
Parametric Polymorphism ◽  
Abstract Data ◽  
Direct Definition ◽  
Semantic Types ◽  
Definition Of

We present a realisability model for a call-by-value, higher-order programming language with parametric polymorphism, general first-class references, and recursive types. The main novelty is a relational interpretation of open types that include general reference types. The interpretation uses a new approach to modelling references.The universe of semantic types consists of world-indexed families of logical relations over a universal predomain. In order to model general reference types, worlds are finite maps from locations to semantic types: this introduces a circularity between semantic types and worlds that precludes a direct definition of either. Our solution is to solve a recursive equation in an appropriate category of metric spaces. In effect, types are interpreted using a Kripke logical relation over a recursively defined set of worlds.We illustrate how the model can be used to prove simple equivalences between different implementations of imperative abstract data types.

scholarly journals Parametric polymorphism and operational equivalence

2000 ◽  
Vol 10 (3) ◽  
pp. 321-359 ◽  
Author(s):  
ANDREW M. PITTS
Keyword(s):  
Programming Language ◽  
Functional Programming ◽  
Closure Operator ◽  
Lambda Calculus ◽  
Logical Relation ◽  
Data Types ◽  
Mathematical Properties ◽  
Parametric Polymorphism ◽  
Operational Behaviour

Studies of the mathematical properties of impredicative polymorphic types have for the most part focused on the polymorphic lambda calculus of Girard–Reynolds, which is a calculus of total polymorphic functions. This paper considers polymorphic types from a functional programming perspective, where the partialness arising from the presence of fixpoint recursion complicates the nature of potentially infinite (‘lazy’) data types. An approach to Reynolds' notion of relational parametricity is developed that works directly on the syntax of a programming language, using a novel closure operator to relate operational behaviour to parametricity properties of types. Working with an extension of Plotkin's PCF with ∀-types, lazy lists and existential types, we show by example how the resulting logical relation can be used to prove properties of polymorphic types up to operational equivalence.

On lists and other abstract data types in the calculus of constructions

2000 ◽  
Vol 10 (2) ◽  
pp. 261-276 ◽  
Author(s):  
JONATHAN P. SELDIN
Keyword(s):  
Data Type ◽  
Abstract Data Type ◽  
Abstract Data Types ◽  
Natural Numbers ◽  
Data Types ◽  
Induction Principle ◽  
Calculus Of Constructions ◽  
Abstract Data ◽  
Definition Of ◽  
Future Work

The representation of the inductively defined abstract data type for lists was left incomplete in Seldin (1997, Section 9). Here that representation is completed, and it is proved that all extra axioms needed are consistent. Among the innovations of this paper is a definition of cdr, whose definition was left for future work in Seldin (1997, Section 9). The results are then extended to other abstract data types – those of Berardi (1993). The method used to define cdr for lists is extended to obtain the definition of an inverse for each argument of each constructor of an abstract data type. These inverses are used to prove the injective property for the constructors. Also, Dedekind's method of defining the natural numbers is used to define a predicate associated with each abstract data type, and the use of this predicate makes it unnecessary to postulate the induction principle. The only axioms left to be proved are those asserting the disjointness of the co-domains of different constructors, and it is shown that those axioms can be proved consistent.

On the Power of Model Theory in Specifying Abstract Data Types and in Capturing Their Recursiveness

1983 ◽  
Vol 6 (2) ◽  
pp. 127-170
Author(s):  
Alberto Bertoni ◽  
Giancarlo Mauri ◽  
Pierangelo Miglioli
Keyword(s):  
Model Theory ◽  
Point Of View ◽  
Necessary Condition ◽  
Abstract Data Type ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data ◽  
Definition Of ◽  
Recursive Data ◽  
Better Than

In this paper a comparative analysis of some algebraic and model-theoretic tools to specify abstract data types is presented: our aim is to show that, in order to capture a quite relevant feature such as the recursiveness of abstract data types, Model Theory works better than Category Theory. To do so, we analyze various notions such as “initiality”, “finality”, “monoinitiality”, “epifinality”, “weak monoinitiality” and “weak epifinality”, both from the point of view of “abstractness” and of “cardinality”, in a general model theoretical frame. For the second aspect, it is shown that only “initiality”, “monoinitiality”, “epifinality” and “weak epifinality” allow us to select countable models (for theories with a countable language), a necessary condition to get recursive data types, while this is not the case for “finality” and “weak monoinitiality”. An extensive analysis is then devoted to the problem of the recursiveness of abstract data types: we provide a formal definition of recursiveness and show that it neither collapses, nor it is incompatible with the “abstractness” requirement. We also show that none of the above quoted categorial notions captures recursiveness. Finally, we consider our own definition of “abstract data type”, based on typically model-theoretic notions, and illustrate the sense according to which it captures recursiveness.

scholarly journals Abstract Semantic Algebras!

1982 ◽  
Vol 11 (145) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Conceptual Analysis ◽  
Formal Description ◽  
Data Types ◽  
New Approach ◽  
Initial Algebra ◽  
Language Semantics ◽  
Abstract Data ◽  
Initial Algebra Semantics

A new approach to the formal description of programming language semantics is described and illustrated. ''Abstract semantic algebras'' are just algebraically-specified abstract data types whose operations correspond to fundamental concepts of programming languages. The values of abstract semantic algebras are taken as meanings of programs in Denotational (or Initial Algebra) Semantics, instead of using Scott domains. This leads to semantic descriptions that clearly exhibit the underlying conceptual analysis, and which are rather easy to modify and extend. Some basic abstract semantic algebras corresponding to fundamental concepts of programming languages are given; they could be used in the description of many different programming languages.

A new approach to abstract data types, I Informal development

1992 ◽  
Vol 2 (2) ◽  
pp. 193-229 ◽  
Author(s):  
Solomon Feferman
Keyword(s):  
Large Scale ◽  
Design Tools ◽  
Modular Construction ◽  
Abstract Data Types ◽  
Data Types ◽  
New Approach ◽  
Abstract Data ◽  
Informal Development ◽  
Data Objects

The concept of abstract data types (ADTs) has emerged in the last fifteen years or so as one of the major programming design tools, with the emphasis on modular construction of large-scale programe. ADTs provide the means for seperating how data objects may be used from the different ways in which they actually are, or might be, implemented. A foundation for the theory of compputation with ADTs must provide answers to such questions as: What are ADTs and how may they be specified? What does it mean to implement an ADT? How may we construct new ADTs from old ones? What does it mean to compute with ADTs? This paper is devoted to a new and rather general, constructively based approach to these questions.

Seeing, imagined, and lived

2020 ◽  
Vol 3 (2) ◽  
Author(s):  
Anandi Silva Knuppel
Keyword(s):  
Sensory Experience ◽  
Religious Practices ◽  
Daily Lives ◽  
New Approach ◽  
Theories Of Practice ◽  
Sources Of Authority ◽  
Definition Of

Scholarship on Hindu traditions and practices proposes the practice of darshan as fundamental to Hindu traditions, particularly in temple worship, observing that devotees seek out images of deities primarily to see them and “receive” their darshan. These works typically gloss the definition of darshan with a sentence or two about seeing, exchanging glances, and/or receiving blessings. In this paper, I focus on the ways in which darshan is ideally imagined in conjunction with other bodily sensory practices through sources of authority, such as texts and senior devotees, to create a specific sensory experience and expectation in the transnational Gaudiya Vaishnava community. I then look to the lived realitiesof darshan in this tradition, specifically how devotees negotiate the structures created through sources of authority in their daily lives. Through this juxtaposition of idealized and lived darshan, I argue that we need a new approach towards theories of practice to take into account the complexities of darshanic moments in this and other religious practices.

Towards the Temporal Approach to Abstract Data Types

1988 ◽  
Vol 11 (1) ◽  
pp. 49-63
Author(s):  
Andrzej Szalas
Keyword(s):  
Temporal Logic ◽  
Abstract Data Types ◽  
Data Types ◽  
First Order ◽  
Abstract Data ◽  
Order Completeness ◽  
General Method

In this paper we deal with a well known problem of specifying abstract data types. Up to now there were many approaches to this problem. We follow the axiomatic style of specifying abstract data types (cf. e.g. [1, 2, 6, 8, 9, 10]). We apply, however, the first-order temporal logic. We introduce a notion of first-order completeness of axiomatic specifications and show a general method for obtaining first-order complete axiomatizations. Some examples illustrate the method.

scholarly journals An Intrinsic Characterization of Five Points in a CAT(0) Space

2020 ◽  
Vol 8 (1) ◽  
pp. 114-165
Author(s):  
Tetsu Toyoda
Keyword(s):  
Metric Space ◽  
Isometric Embedding ◽  
Metric Spaces ◽  
Necessary Conditions ◽  
New Approach ◽  
Intrinsic Characterization ◽  
New Family

AbstractGromov (2001) and Sturm (2003) proved that any four points in a CAT(0) space satisfy a certain family of inequalities. We call those inequalities the ⊠-inequalities, following the notation used by Gromov. In this paper, we prove that a metric space X containing at most five points admits an isometric embedding into a CAT(0) space if and only if any four points in X satisfy the ⊠-inequalities. To prove this, we introduce a new family of necessary conditions for a metric space to admit an isometric embedding into a CAT(0) space by modifying and generalizing Gromov’s cycle conditions. Furthermore, we prove that if a metric space satisfies all those necessary conditions, then it admits an isometric embedding into a CAT(0) space. This work presents a new approach to characterizing those metric spaces that admit an isometric embedding into a CAT(0) space.

Sign in / Sign up

Export Citation Format

Share Document