Abstract

This paper collects observations about the two issues of sequentiality and full abstraction for programming languages. The format of the paper is that of an extended lecture. Some old and new results are hinted at, and references are given, without any claim to be exhaustive. We assume that the reader knows something about λ-calculus and about domain theory.

Introduction

Sequentiality and full abstraction have been often considered as related topics. More precisely, the quest of full abstraction led to the idea that sequentiality is a key issue in the semantics of programming languages.

In vague terms, full abstraction is the property that a mathematical semantics captures exactly the operational semantics of a specific language under study. Following the tradition of the first studies on full abstraction [Milner,Plotkin], the languages considered here are PCF, an extension of λ-calculus with arithmetic operators and recursion, and variants thereof. The focus on λ-calculus is amply justified by its rôle, either as a kernel (functional) programming language, or as a suitable metalanguage for the encoding of denotational semantics of a great variety of (sequential) programming languages.

It was Gérard Berry's belief that only after a detailed sudy of the syntax could one conceive the semantic definitions appropriate for reaching full abstraction. I always considered this as an illuminating idea, and this will be the starting point of this paper.

In section 2, we shall state Berry's Sequentiality Theorem: this will require us first to recall Wadsworth-Welch-Lévy's Continuity Theorem, and then to introduce a general notion of sequential function, due to Kahn-Plotkin.

In section 3, we shall abandon sequentiality for a while to define full abstraction and quote some results.