Equational properties of stratified least fixed points

TL;DR

This paper investigates a new fixed point operation for non-monotonic functions on stratified lattices, demonstrating it satisfies standard fixed point identities and exploring its relation to lambda-abstraction.

Contribution

It proves that the novel fixed point operation adheres to iteration theory axioms and analyzes its properties in the context of lambda-abstraction.

Findings

The new fixed point operation satisfies standard fixed point identities.

It connects the fixed point operation with lambda-abstraction.

Provides theoretical foundations for semantics of logic programs with negation.

Abstract

Recently, a novel fixed point operation has been introduced over certain non-monotonic functions between stratified complete lattices and used to give semantics to logic programs with negation and boolean context-free grammars. We prove that this new operation satisfies `the standard' identities of fixed point operations as described by the axioms of iteration theories. We also study this new fixed point operation in connection with lambda-abstraction.