Typed SLD-Resolution: Dynamic Typing for Logic Programming

TL;DR

This paper introduces TSLD-resolution, a new operational semantics for logic programming that incorporates dynamic type error detection during execution, bridging operational and declarative semantics.

Contribution

It defines TSLD-resolution with a typed unification algorithm and proves its correctness relative to a typed declarative semantics.

Findings

TSLD-resolution detects runtime type errors.

A typed unification algorithm is developed.

Correctness of TSLD-resolution is formally proven.

Abstract

The semantic foundations for logic programming are usually separated into two different approaches. The operational semantics, which uses SLD-resolution, the proof method that computes answers in logic programming, and the declarative semantics, which sees logic programs as formulas and its semantics as models. Here, we define a new operational semantics called TSLD-resolution, which stands for Typed SLD-resolution, where we include a value "wrong", that corresponds to the detection of a type error at run-time. For this we define a new typed unification algorithm. Finally we prove the correctness of TSLD-resolution with respect to a typed declarative semantics.