Iterative miniKanren in multiple languages

Motivation

The Codex Bezae is an ancient-era handwritten book where each left-side page of Greek has a translation into Latin on the right-side page. It is digitized at https://cudl.lib.cam.ac.uk/view/MS-NN-00002-00041. It was immensely helpful for me when I was studying Greek and Latin. The Biblical vocabulary and grammar was plain and I had two translations to work with.

I want to do something similar with this project. I hope you can learn something from similar code written in multiple programming languages.

Since this document is read from top to bottom by the Bezae compiler, all import statements must be included first. 

from typing import List
from dataclasses import dataclass


#include <stdlib.h>
#include <stdbool.h>
#include <string.h>

What is an S-Expression?

An S-Expression (here on referred to as a SExp) is either an atom, or a pair. All atoms will be represented as a symbol, and for most languages, a symbol is just a string. 

Symbol = str


typedef char* Symbol;


type Symbol = string


type Symbol = String
The pair case of SExp is more complicated, because it contains two SExps as children. S-Expressions come from Lisp, and in Lisp, this pair case is called a cons pair, where the left child is called car and the right child is called cdr. 

@dataclass
class Sym:
    sym: Symbol

@dataclass
class Cons:
    car: 'SExp'
    cdr: 'SExp'

SExp = Sym | Cons


type SExp = {
    kind: 'SYMBOL',
    sym: Symbol
} | {
    kind: 'CONS',
    car: SExp,
    cdr: SExp
}


data SExp = Sym Symbol | Cons SExp SExp


enum SExpTag { SYMBOL, CONS };

struct SExp {
    enum SExpTag kind;
    union {
        // kind == SYMBOL
        struct {
            Symbol sym;
        };
        // kind == CONS
        struct {
            struct SExp *car;
            struct SExp *cdr;
        };
    };
};

// It would be useful to have some constructors as well

struct SExp *make_Cons(struct SExp *car, struct SExp *cdr) {
    struct SExp *result = malloc(sizeof(struct SExp));
    result->kind = CONS;
    result->car = car;
    result->cdr = cdr;
    return result;
}

Does the symbol occur anywhere in the SExp?

Given: a Symbol and a SExp, returns true if the SExp contains the same symbol (that is, a string with the same contents). 

def symbol_occurs_in_sexp(x: Symbol, sexp: SExp) -> bool:
    match sexp:
        case Sym(sym):
            return x == sym

        case Cons(car, cdr):
            return (
                symbol_occurs_in_sexp(x, car) or
                symbol_occurs_in_sexp(x, cdr)
            )


bool symbol_occurs_in_sexp(Symbol x, struct SExp *sexp) {
    switch (sexp->kind) {
        case SYMBOL:
            return strcmp(x, sexp->sym) == 0;

        case CONS:
            return (
                symbol_occurs_in_sexp(x, sexp->car) ||
                symbol_occurs_in_sexp(x, sexp->cdr)
            );
    }
}


symbolOccursInSexp :: Symbol -> SExp -> Bool
symbolOccursInSexp x sexp = case sexp of
    (Sym sym) -> x == sym

    (Cons car cdr) ->
        symbolOccursInSexp x car ||
        symbolOccursInSexp x cdr

Replace symbol in a SExp

Given a symbol, an s-expression replacement, and an s-expression body, returns a new s-expression body with all occurrences of the symbol replaced with the s-expression. 

replaceSymbolInSExp :: Symbol -> SExp -> SExp -> SExp
replaceSymbolInSExp replaceMe replaceWith sexp = case sexp of
    (Sym sym) -> if sym == replaceMe
        then replaceWith
        else Sym sym
    (Cons car cdr) -> Cons
        (replaceSymbolInSExp replaceMe replaceWith car)
        (replaceSymbolInSExp replaceMe replaceWith cdr)


def replace_symbol_in_sexp(replace_me: Symbol, replace_with: SExp, sexp: SExp) -> SExp:
    match sexp:
        case Sym(sym):
            if sym == replace_me:
                return replace_with
            else:
                return Sym(sym)

        case Cons(car, cdr):
            return Cons(
                replace_symbol_in_sexp(replace_me, replace_with, car),
                replace_symbol_in_sexp(replace_me, replace_with, cdr)
            )


struct SExp *replace_symbol_in_sexp(Symbol replace_me, struct SExp *replace_with, struct SExp *sexp) {
    switch (sexp->kind) {
        case SYMBOL:
            return (strcmp(sexp->sym, replace_me) == 0)
                ? replace_with
                : sexp;

        case CONS:
            return make_Cons(
                replace_symbol_in_sexp(replace_me, replace_with, sexp->car),
                replace_symbol_in_sexp(replace_me, replace_with, sexp->cdr)
            );
    }
}

miniKanren and the definition of a clause

For my purposes, the definition of a miniKanren clause is best described in Haskell: 

data Clause
    = Relation Symbol [SExp]
    | Conde [[Clause]]
    | Fresh [Symbol] [Clause]


@dataclass
class Relation:
    name: Symbol
    args: List[SExp]

@dataclass
class Conde:
    conjunctions: List[List['Clause']]

@dataclass
class Fresh:
    vars: List[Symbol]
    clauses: List['Clause']

Clause = Relation | Conde | Fresh


enum ClauseTag { RELATION, CONDE, FRESH };

struct Clause {
    enum ClauseTag kind;

    union {
        // kind == RELATION
        struct {
            Symbol name;
            struct SExp *args;
            int num_args;
        };

        // kind == CONDE
        struct {
            struct Clause **conjunctions;
            int *nums_clauses;
            int num_conjunctions;
        };

        // kind == FRESH
        struct {
            Symbol *vars;
            int num_vars;
            struct Clause *clauses;
            int num_clauses;
        };
    };
};

Replace symbol with s-expression in a miniKanren clause

Given a symbol, an SExp to replace it with, and a miniKanren clause, produce a new clause with all occurrences of the symbol replaced with the s-expression. But it must also respect lexical scope: if a fresh clause defines an identical symbol, do not replace in the fresh body, because the symbol has been shadowed. 

replaceSymbolInClause :: Symbol -> SExp -> Clause -> Clause
replaceSymbolInClause replaceMe replaceWith clause = case clause of
    Relation name args ->
        Relation name (map (replaceSymbolInSExp replaceMe replaceWith) args)

    Conde conjunctions ->
        Conde (map (map (replaceSymbolInClause replaceMe replaceWith)) conjunctions)

    Fresh vars clauses ->
        if replaceMe `elem` vars
        then Fresh vars clauses
        else Fresh vars (map (replaceSymbolInClause replaceMe replaceWith) clauses)


def replace_symbol_in_clause(replace_me: Symbol, replace_with: SExp, clause: Clause) -> Clause:
    match clause:
        case Relation(name, args):
            return Relation(name, [replace_symbol_in_sexp(replace_me, replace_with, arg) for arg in args])

        case Conde(conjunctions):
            return Conde([[replace_symbol_in_clause(replace_me, replace_with, clause)
                for clause in conjunction]
                for conjunction in conjunctions
            ])

        case Fresh(vars, clauses):
            if replace_me in vars:
                return Fresh(vars, clauses)
            else:
                return Fresh(vars, [
                    replace_symbol_in_clause(replace_me, replace_with, clause)
                    for clause in clauses
                ])


struct SExp *replace_symbol_in_clause(Symbol replace_me, struct SExp *replace_with, struct Clause *clause) {
    switch (clause->kind) {
        case RELATION:
            int n = clause->num_args;
            struct Clause *result = malloc(sizeof(struct Clause));
            result->kind = RELATION;
            result->num_args = n;
            result->args = malloc(sizeof(struct SExp *) * n);
            for (int i = 0; i < n; i++) {
                result->args[i] = replace_symbol_in_sexp(replace_me, replace_with, clause->args[i]);
            }

            return result;

        case CONDE:
            int n = clause->num_conjunctions;
            struct Clause *result = malloc(sizeof(struct Clause));
            result->kind = RELATION;
            result->num_conjunctions = n;
            result->nums_clauses = clause->nums_clauses;
            result->conjunctions = malloc(sizeof(struct Clause *) * n);
            for (int i = 0; i < n; i++) {
                int m = clause->nums_clauses[i];
                for (int j = 0; j < m; j++) {
                    result->conjunctions[i * n + j] = replace_symbol_in_clause(
                        replace_me, replace_with,
                        clause->conjunctions[i * n + j]
                    );
                }
            }

            return result;

        case FRESH:
            for (int i = 0; i < clause->num_vars; i++) {
                if (strcmp(replace_me, clause->vars[i]) == 0) {
                    return clause;
                }
            }

            struct Clause *result = malloc(sizeof(struct Clause));
            

            return;
    }
}

defrel, run, and run*

The final pieces of miniKanren syntax allow us to define and run relations. 

data Defrel = Defrel Symbol [Symbol] [Clause]


@dataclass
class Defrel:
    name: Symbol
    args: List[Symbol]
    clauses: List[Clause]

The appendo relation

Having defined all the miniKanren keywords, I can now write the classic appendo relation. 

'(defrel (appendo l r o)
    (conde
        ((== l '()) (== r o))
        ((fresh (h t rec)
            (== l `(,h . ,t))
            (== o `(,h . ,rec))
            (appendo t r rec)))))


appendo = Defrel('appendo', ['l', 'r', 'o'], [
    Conde([
        [Relation('==', [Sym('l'), Sym('nil')]), Relation('==', [Sym('r'), Sym('o')])],
        [Fresh(['h', 't', 'rec'], [
            Relation('==', [Sym('l'), Cons(Sym('h'), Sym('t'))]),
            Relation('==', [Sym('o'), Cons(Sym('h'), Sym('rec'))]),
            Relation('appendo', [Sym('t'), Sym('r'), Sym('rec')])])]])])