Synthesis of models for order-sorted first-order theories using linear algebra and constraint solving

TL;DR

This paper presents a method for automatically generating numerical models for order-sorted first-order logics using linear algebra and constraint solving, aiding in termination analysis of declarative programs.

Contribution

It introduces a novel approach combining convex domains and matrix interpretations to synthesize models for order-sorted first-order theories.

Findings

Effective numerical models can be generated using linear algebra techniques.

Models facilitate termination analysis of declarative programs.

The approach leverages existing constraint solving tools.

Abstract

Recent developments in termination analysis for declarative programs emphasize the use of appropriate models for the logical theory representing the program at stake as a generic approach to prove termination of declarative programs. In this setting, Order-Sorted First-Order Logic provides a powerful framework to represent declarative programs. It also provides a target logic to obtain models for other logics via transformations. We investigate the automatic generation of numerical models for order-sorted first-order logics and its use in program analysis, in particular in termination analysis of declarative programs. We use convex domains to give domains to the different sorts of an order-sorted signature; we interpret the ranked symbols of sorted signatures by means of appropriately adapted convex matrix interpretations. Such numerical interpretations permit the use of existing algorithms and tools from linear algebra and arithmetic constraint solving to synthesize the models.