webyrd/declarative-semantics

miniKanren implementation of ' Declarative semantics for functional languages: compositional, extensional, and elementary' by Jeremy Siek.

Source code at GitHub null

{
  "createdAt": "2017-09-06T00:49:05Z",
  "defaultBranch": "master",
  "description": "miniKanren implementation of ' Declarative semantics for functional languages: compositional, extensional, and elementary' by Jeremy Siek.",
  "fullName": "webyrd/declarative-semantics",
  "homepage": null,
  "language": "Scheme",
  "name": "declarative-semantics",
  "pushedAt": "2018-03-16T22:49:19Z",
  "stargazersCount": 15,
  "topics": [],
  "updatedAt": "2025-07-08T01:23:57Z",
  "url": "https://github.com/webyrd/declarative-semantics"
}

declarative-semantics

miniKanren prototype of version v2 of ‘Declarative semantics for functional languages: compositional, extensional, and elementary’ by Jeremy Siek.

Important: the code in this repository is from an older version (version v2) of Jeremy’s paper. The latest version of the preprint can be found here ‘Declarative semantics for functional languages: compositional, extensional, and elementary’ but is quite different from version v2. For example, figure 2 from version 2 is no longer in the latest version of the paper, as of 14 March 02018.

Code written by Ramana Kumar, Tim Zakian, and Will Byrd, after discussion with Jeremy Siek.

The code implements the interesting parts of Figure 2 on page 7 of the paper. See the tests in tables-subsets.scm for an idea of what the queries and answers look like.

There are currently two versions of the code:

tables-subsets.scm, which is the closer of the two implementations to the spirit of Figure 2. The Subset relation is explicit.
tables.scm, in which the subset relation is implicit.

tables-subsets.scm seems to be closer to the spirit of Figure 2.

Questions/Future Work:

Are the two implementations equivalent?
Is there a way to avoid generating “duplicate” tables, perhaps through tabling or through laziness/new constraints?
Implement the rest of the paper.
Explore how well this version of the relational interpreter works for problems we care about (quines, recursive program synthesis, etc.).

Here is an example showing 100 tables resulting from evaluating (lambda (x) x):

Chez Scheme Version 9.4.1
Copyright 1984-2017 Cisco Systems, Inc.

> (load "tables-subsets.scm")
Testing subseto-1
Testing subseto-2
Testing subseto-3
Testing subseto-4
Testing subseto-5
Testing subseto-6
Testing subseto-7
Testing subseto-8
Testing subset-9
Testing evalo-1
Testing evalo-2
Testing evalo-3
Testing evalo-4
Testing evalo-5
Testing evalo-6
=====================
=====================

=====================
_.0 -> _.0
---------------------
((num _.0))
=====================

=====================
() -> ()
=====================

=====================
_.0 -> _.0
_.1 -> _.1
---------------------
((num _.0 _.1))
=====================

=====================
(_.0 . _.1) -> ()
=====================

=====================
_.0 -> _.0
() -> ()
---------------------
((num _.0))
=====================

=====================
(_.0 . _.1) -> (_.0 . _.1)
---------------------
((num _.1))
=====================

=====================
() -> ()
_.0 -> _.0
---------------------
((num _.0))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
---------------------
((num _.0 _.1 _.2))
=====================

=====================
_.0 -> _.0
(_.1 . _.2) -> ()
---------------------
((num _.0))
=====================

=====================
() -> ()
() -> ()
=====================

=====================
_.0 -> _.0
_.1 -> _.1
() -> ()
---------------------
((num _.0 _.1))
=====================

=====================
_.0 -> _.0
(_.1 . _.2) -> (_.1 . _.2)
---------------------
((num _.0 _.2))
=====================

=====================
(_.0 . _.1) -> ()
_.2 -> _.2
---------------------
((num _.2))
=====================

=====================
_.0 -> _.0
() -> ()
_.1 -> _.1
---------------------
((num _.0 _.1))
=====================

=====================
() -> ()
_.0 -> _.0
_.1 -> _.1
---------------------
((num _.0 _.1))
=====================

=====================
(_.0) -> (_.0)
=====================

=====================
() -> ()
(_.0 . _.1) -> ()
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
_.3 -> _.3
---------------------
((num _.0 _.1 _.2 _.3))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
(_.2 . _.3) -> ()
---------------------
((num _.0 _.1))
=====================

=====================
(_.0 . _.1) -> ()
() -> ()
=====================

=====================
_.0 -> _.0
() -> ()
() -> ()
---------------------
((num _.0))
=====================

=====================
() -> ()
_.0 -> _.0
() -> ()
---------------------
((num _.0))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
() -> ()
---------------------
((num _.0 _.1 _.2))
=====================

=====================
(_.0 . _.1) -> (_.0 . _.1)
_.2 -> _.2
---------------------
((num _.1 _.2))
=====================

=====================
() -> ()
(_.0 . _.1) -> (_.0 . _.1)
---------------------
((num _.1))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
(_.2 . _.3) -> (_.2 . _.3)
---------------------
((num _.0 _.1 _.3))
=====================

=====================
_.0 -> _.0
(_.1 . _.2) -> ()
_.3 -> _.3
---------------------
((num _.0 _.3))
=====================

=====================
() -> ()
() -> ()
_.0 -> _.0
---------------------
((num _.0))
=====================

=====================
(_.0 _.1 . _.2) -> (_.1 . _.2)
---------------------
((=/= ((_.0 _.1))) (num _.2))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
() -> ()
_.2 -> _.2
---------------------
((num _.0 _.1 _.2))
=====================

=====================
(_.0 . _.1) -> ()
_.2 -> _.2
_.3 -> _.3
---------------------
((num _.2 _.3))
=====================

=====================
_.0 -> _.0
() -> ()
_.1 -> _.1
_.2 -> _.2
---------------------
((num _.0 _.1 _.2))
=====================

=====================
(_.0 . _.1) -> ()
(_.2 . _.3) -> ()
=====================

=====================
() -> ()
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
---------------------
((num _.0 _.1 _.2))
=====================

=====================
_.0 -> _.0
(_.1) -> (_.1)
---------------------
((num _.0))
=====================

=====================
_.0 -> _.0
() -> ()
(_.1 . _.2) -> ()
---------------------
((num _.0))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
_.3 -> _.3
_.4 -> _.4
---------------------
((num _.0 _.1 _.2 _.3 _.4))
=====================

=====================
(_.0 . _.1) -> (_.0 . _.1)
() -> ()
---------------------
((num _.1))
=====================

=====================
() -> ()
_.0 -> _.0
(_.1 . _.2) -> ()
---------------------
((num _.0))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
(_.3 . _.4) -> ()
---------------------
((num _.0 _.1 _.2))
=====================

=====================
_.0 -> _.0
(_.1 . _.2) -> ()
() -> ()
---------------------
((num _.0))
=====================

=====================
() -> ()
() -> ()
() -> ()
=====================

=====================
_.0 -> _.0
_.1 -> _.1
() -> ()
() -> ()
---------------------
((num _.0 _.1))
=====================

=====================
(_.0 . _.1) -> ()
_.2 -> _.2
() -> ()
---------------------
((num _.2))
=====================

=====================
_.0 -> _.0
() -> ()
_.1 -> _.1
() -> ()
---------------------
((num _.0 _.1))
=====================

=====================
() -> ()
_.0 -> _.0
_.1 -> _.1
() -> ()
---------------------
((num _.0 _.1))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
_.3 -> _.3
() -> ()
---------------------
((num _.0 _.1 _.2 _.3))
=====================

=====================
_.0 -> _.0
(_.1 . _.2) -> (_.1 . _.2)
_.3 -> _.3
---------------------
((num _.0 _.2 _.3))
=====================

=====================
(_.0 . _.1) -> ()
(_.2 . _.3) -> (_.2 . _.3)
---------------------
((num _.3))
=====================

=====================
_.0 -> _.0
() -> ()
(_.1 . _.2) -> (_.1 . _.2)
---------------------
((num _.0 _.2))
=====================

=====================
() -> ()
_.0 -> _.0
(_.1 . _.2) -> (_.1 . _.2)
---------------------
((num _.0 _.2))
=====================

=====================
(_.0) -> (_.0)
_.1 -> _.1
---------------------
((num _.1))
=====================

=====================
() -> ()
(_.0 . _.1) -> ()
_.2 -> _.2
---------------------
((num _.2))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
(_.3 . _.4) -> (_.3 . _.4)
---------------------
((num _.0 _.1 _.2 _.4))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
(_.2 . _.3) -> ()
_.4 -> _.4
---------------------
((num _.0 _.1 _.4))
=====================

=====================
(_.0 . _.1) -> ()
() -> ()
_.2 -> _.2
---------------------
((num _.2))
=====================

=====================
_.0 -> _.0
() -> ()
() -> ()
_.1 -> _.1
---------------------
((num _.0 _.1))
=====================

=====================
_.0 -> _.0
(_.1 _.2 . _.3) -> (_.2 . _.3)
---------------------
((=/= ((_.1 _.2))) (num _.0 _.3))
=====================

=====================
() -> ()
_.0 -> _.0
() -> ()
_.1 -> _.1
---------------------
((num _.0 _.1))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
() -> ()
_.3 -> _.3
---------------------
((num _.0 _.1 _.2 _.3))
=====================

=====================
(_.0 . _.1) -> (_.0 . _.1)
_.2 -> _.2
_.3 -> _.3
---------------------
((num _.1 _.2 _.3))
=====================

=====================
_.0 -> _.0
(_.1 . _.2) -> ()
_.3 -> _.3
_.4 -> _.4
---------------------
((num _.0 _.3 _.4))
=====================

=====================
() -> ()
() -> ()
_.0 -> _.0
_.1 -> _.1
---------------------
((num _.0 _.1))
=====================

=====================
(_.0 _.1 . _.2) -> (_.0)
=====================

=====================
(_.0 . _.1) -> (_.0 . _.1)
(_.2 . _.3) -> ()
---------------------
((num _.1))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
() -> ()
_.2 -> _.2
_.3 -> _.3
---------------------
((num _.0 _.1 _.2 _.3))
=====================

=====================
(_.0 . _.1) -> ()
_.2 -> _.2
_.3 -> _.3
_.4 -> _.4
---------------------
((num _.2 _.3 _.4))
=====================

=====================
() -> ()
(_.0) -> (_.0)
=====================

=====================
_.0 -> _.0
(_.1 . _.2) -> ()
(_.3 . _.4) -> ()
---------------------
((num _.0))
=====================

=====================
_.0 -> _.0
() -> ()
_.1 -> _.1
_.2 -> _.2
_.3 -> _.3
---------------------
((num _.0 _.1 _.2 _.3))
=====================

=====================
() -> ()
() -> ()
(_.0 . _.1) -> ()
=====================

=====================
_.0 -> _.0
_.1 -> _.1
(_.2) -> (_.2)
---------------------
((num _.0 _.1))
=====================

=====================
() -> ()
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
_.3 -> _.3
---------------------
((num _.0 _.1 _.2 _.3))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
() -> ()
(_.2 . _.3) -> ()
---------------------
((num _.0 _.1))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
_.3 -> _.3
_.4 -> _.4
_.5 -> _.5
---------------------
((num _.0 _.1 _.2 _.3 _.4 _.5))
=====================

=====================
_.0 -> _.0
(_.1 . _.2) -> (_.1 . _.2)
() -> ()
---------------------
((num _.0 _.2))
=====================

=====================
(_.0 . _.1) -> ()
_.2 -> _.2
(_.3 . _.4) -> ()
---------------------
((num _.2))
=====================

=====================
_.0 -> _.0
() -> ()
_.1 -> _.1
(_.2 . _.3) -> ()
---------------------
((num _.0 _.1))
=====================

=====================
() -> ()
_.0 -> _.0
_.1 -> _.1
(_.2 . _.3) -> ()
---------------------
((num _.0 _.1))
=====================

=====================
(_.0) -> (_.0)
() -> ()
=====================

=====================
() -> ()
(_.0 . _.1) -> ()
() -> ()
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
_.3 -> _.3
(_.4 . _.5) -> ()
---------------------
((num _.0 _.1 _.2 _.3))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
(_.2 . _.3) -> ()
() -> ()
---------------------
((num _.0 _.1))
=====================

=====================
(_.0 . _.1) -> ()
() -> ()
() -> ()
=====================

=====================
_.0 -> _.0
() -> ()
() -> ()
() -> ()
---------------------
((num _.0))
=====================

=====================
() -> ()
_.0 -> _.0
() -> ()
() -> ()
---------------------
((num _.0))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
() -> ()
() -> ()
---------------------
((num _.0 _.1 _.2))
=====================

=====================
(_.0 . _.1) -> (_.0 . _.1)
_.2 -> _.2
() -> ()
---------------------
((num _.1 _.2))
=====================

=====================
_.0 -> _.0
(_.1 . _.2) -> ()
_.3 -> _.3
() -> ()
---------------------
((num _.0 _.3))
=====================

=====================
() -> ()
() -> ()
_.0 -> _.0
() -> ()
---------------------
((num _.0))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
() -> ()
_.2 -> _.2
() -> ()
---------------------
((num _.0 _.1 _.2))
=====================

=====================
(_.0 . _.1) -> ()
_.2 -> _.2
_.3 -> _.3
() -> ()
---------------------
((num _.2 _.3))
=====================

=====================
_.0 -> _.0
() -> ()
_.1 -> _.1
_.2 -> _.2
() -> ()
---------------------
((num _.0 _.1 _.2))
=====================

=====================
() -> ()
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
() -> ()
---------------------
((num _.0 _.1 _.2))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
_.2 -> _.2
_.3 -> _.3
_.4 -> _.4
() -> ()
---------------------
((num _.0 _.1 _.2 _.3 _.4))
=====================

=====================
() -> ()
(_.0 . _.1) -> (_.0 . _.1)
_.2 -> _.2
---------------------
((num _.1 _.2))
=====================

=====================
(_.0 . _.1) -> (_.0 . _.1)
(_.2 . _.3) -> (_.2 . _.3)
---------------------
((num _.1 _.3))
=====================

=====================
_.0 -> _.0
_.1 -> _.1
(_.2 . _.3) -> (_.2 . _.3)
_.4 -> _.4
---------------------
((num _.0 _.1 _.3 _.4))
=====================

=====================
(_.0 _.1 . _.2) -> (_.1 . _.2)
_.3 -> _.3
---------------------
((=/= ((_.0 _.1))) (num _.2 _.3))
=====================