Deriving Abstract Semantics for Forward Analysis of Normal Logic Programs

TL;DR

This paper introduces two formal fixed-point abstract semantics for forward analysis of normal logic programs, addressing a gap in the formal understanding of negation as failure in abstract interpretation.

Contribution

It proposes the first formal semantics specifically designed for forward abstract interpretation of normal logic programs, including negation as failure.

Findings

Defines two generic fixed-point semantics, $F^b$ and $F^ riangle$, for normal logic programs.

Provides a formal foundation for inferring data descriptions in program graphs and textual program points.

Addresses a previously unformalized aspect of logic program analysis.

Abstract

The problem of forward abstract interpretation of {\em normal} logic programs has not been formally addressed in the literature although negation as failure is dealt with through the built-in predicate ! in the way it is implemented in Prolog. This paper proposes a solution to this problem by deriving two generic fixed-point abstract semantics $F^b and $F^\diamond for forward abstract interpretation of {\em normal} logic programs. $F^b$ is intended for inferring data descriptions for edges in the program graph where an edge denotes the possibility that the control of execution transfers from its source program point to its destination program point. $F^\diamond$ is derived from $F^b$ and is intended for inferring data descriptions for textual program points.