Full Abstraction for a Recursively Typed Lambda Calculus with Parallel Conditional

TL;DR

This paper develops a denotational semantics for a recursively typed lambda calculus with a parallel conditional, proving full abstraction and confluence, and introduces prime systems for interpreting recursive types.

Contribution

It introduces a fully abstract denotational semantics for a recursive lambda calculus with parallel conditional using prime systems and proves the Approximation Theorem.

Findings

The calculus's reduction relation is confluent.

The semantics is adequate for Boolean observation.

The semantics achieves full abstraction with parallel case-function.

Abstract

We define the syntax and reduction relation of a recursively typed lambda calculus with a parallel case-function (a parallel conditional). The reduction is shown to be confluent. We interpret the recursive types as information systems in a restricted form, which we call prime systems. A denotational semantics is defined with this interpretation. We define the syntactical normal form approximations of a term and prove the Approximation Theorem: The semantics of a term equals the limit of the semantics of its approximations. The proof uses inclusive predicates (logical relations). The semantics is adequate with respect to the observation of Boolean values. It is also fully abstract in the presence of the parallel case-function.