λProlog Bridge to DAMF

λProlog is a logic programming language that extends Prolog in a number of ways. In particular, it has a built-in and declarative treatment of term-level bindings. For more about λProlog, see:

• The λProlog home page
• The book Programming with Higher-Order Logic by D. Miller and G. Nadathur describes the logic, design, and applications for λProlog.

There are two main implementations of λProlog.

• ELPI: an embeddable λProlog interpreter. Version 1.16.7 was released on 20 October 2022.
• Teyjus compiler of λProlog. Version 2.1.1 was released on 7 February 2023.

Producing JSON for Dispatch

The λProlog code for producing JSON objects suitable for Dispatch are as follows:

The following description assumes that one is using the Teyjus compiler for λProlog and that all the .mod files are compiled and linked.

The process for generating JSON involves the following additional files, all based on a common name, here written as FILE. There are three input files (the first three described here) and one output file.

• FILE.sig - the kind/type declarations needed
• FILE.mod - find here the lambda Prolog clauses
• FILE.goals - these are the named goals that will be printed as theorems.
• FILE.json - the output file for Dispatch

Currently, the specific instructions to use this code are the following:

• Add accumlate FILE. to harness.mod
• Add accum_sig FILE. to harness.sig
• Run both tjcc and tjsim on FILE, eg: > tjcc arith ; tjlink arith
• Make sure that FILE.goals has no blank lines.
• Compile and run:

  tjcc harness ; tjlink harness ; tjsim harness
  

• Issue the goal: json FILE.
• The result is FILE.json.

Toplevel command in tjsim, once harness and associated modules have been compiled and loaded:

> tjsim harness
?- json "FILE".

This usage of λProlog is illustrated in the walkthrough.