A Lambda Prolog Based Animation of Twelf Specifications

TL;DR

This paper presents a method to animate Twelf specifications by translating LF expressions into Lambda Prolog, enabling execution and query processing while preserving the ability to recover LF expressions from Lambda Prolog results.

Contribution

It introduces a lossy translation from LF to Lambda Prolog and an inverse translation, allowing Twelf-like behavior to be emulated within Lambda Prolog implementations.

Findings

Successful translation of LF to Lambda Prolog enables animation of specifications.

The inverse translation accurately recovers LF expressions from Lambda Prolog results.

Supports Twelf's query features with unspecified parts and meta-variables.

Abstract

Specifications in the Twelf system are based on a logic programming interpretation of the Edinburgh Logical Framework or LF. We consider an approach to animating such specifications using a Lambda Prolog implementation. This approach is based on a lossy translation of the dependently typed LF expressions into the simply typed lambda calculus (STLC) terms of Lambda Prolog and a subsequent encoding of lost dependency information in predicates that are defined by suitable clauses. To use this idea in an implementation of logic programming a la Twelf, it is also necessary to translate the results found for Lambda Prolog queries back into LF expressions. We describe such an inverse translation and show that it has the necessary properties to facilitate an emulation of Twelf behavior through our translation of LF specifications into Lambda Prolog programs. A characteristic of Twelf is that it permits queries to consist of types which have unspecified parts represented by meta-variables for which values are to be found through computation. We show that this capability can be supported within our translation based approach to animating Twelf specifications.