Inductive and Coinductive Predicate Liftings for Effectful Programs

TL;DR

This paper develops a formal framework using inductive and coinductive predicate liftings to analyze the behavior of effectful higher-order recursive programs, enabling reasoning about total and partial correctness.

Contribution

It introduces a dual approach with inductive and coinductive predicate liftings for effectful programs, formalized in Agda, and develops a logic for behavioral properties including negation and program equivalence.

Findings

Framework formalized in Agda for effectful programs.

Predicate liftings capture total and partial correctness.

Logic subsumes a notion of bisimilarity.

Abstract

We formulate a framework for describing behaviour of effectful higher-order recursive programs. Examples of effects are implemented using effect operations, and include: execution cost, nondeterminism, global store and interaction with a user. The denotational semantics of a program is given by a coinductive tree in a monad, which combines potential return values of the program in terms of effect operations. Using a simple test logic, we construct two sorts of predicate liftings, which lift predicates on a result type to predicates on computations that produce results of that type, each capturing a facet of program behaviour. Firstly, we study inductive predicate liftings which can be used to describe effectful notions of total correctness. Secondly, we study coinductive predicate liftings, which describe effectful notions of partial correctness. The two constructions are dual in the sense that one can be used to disprove the other. The predicate liftings are used as a basis for an endogenous logic of behavioural properties for higher-order programs. The program logic has a derivable notion of negation, arising from the duality of the two sorts of predicate liftings, and it generates a program equivalence which subsumes a notion of bisimilarity. Appropriate definitions of inductive and coinductive predicate liftings are given for a multitude of effect examples. The whole development has been fully formalized in the Agda proof assistant.