A fix-point characterization of Herbrand equivalence of expressions in data flow frameworks

TL;DR

This paper develops a new lattice-theoretic fix-point formulation for Herbrand equivalence in data flow analysis, providing a rigorous mathematical foundation that aligns with classical definitions and enhances understanding of program term equivalences.

Contribution

It introduces an axiomatic, fix-point based lattice framework for Herbrand equivalence, extending classical path-based definitions to an infinite concrete lattice setting.

Findings

Reformulates Herbrand equivalence as a maximum fix point over a concrete lattice.

Establishes the equivalence between the classical meet-over-all-paths and the new fix-point characterization.

Provides a rigorous mathematical foundation for program analysis of term equivalences.

Abstract

The problem of determining Herbrand equivalence of terms at each program point in a data flow framework is a central and well studied question in program analysis. Most of the well-known algorithms for the computation of Herbrand equivalence in data flow frameworks proceed via iterative fix-point computation on some abstract lattice of short expressions relevant to the given flow graph. However the mathematical definition of Herbrand equivalence is based on a meet over all path characterization over the (infinite) set of all possible expressions. The aim of this paper is to develop a lattice theoretic fix-point formulation of Herbrand equivalence on the (infinite) concrete lattice defined over the set of all terms constructible from variables, constants and operators of a program. The present characterization uses an axiomatic formulation of the notion of Herbrand congruence and defines the (infinite) concrete lattice of Herbrand congruences. Transfer functions and non-deterministic assignments are formulated as monotone functions over this concrete lattice. Herbrand equivalence is defined as the maximum fix point of a composite transfer function defined over an appropriate product lattice of the above concrete lattice. A re-formulation of the classical meet-over-all-paths definition of Herbrand equivalence in the above lattice theoretic framework is also presented and is proven to be equivalent to the new lattice theoretic fix-point characterization.