Infinite Pizza

What is logic programming?

• a programming paradigm based on formal logic
• declarative
• languages: Prolog, Datalog, Mercury

µKanren

• μKanren: A Minimal Functional Core for Relational Programming - Jason Hemann, Daniel P. Friedman
• embedded - defined in and executed from a host language (🐍)
• implementations available for many host languages!

My implementation

pip install microkanren

https://github.com/jams2/microkanren/

Using µKanren

🏃 + 🥅 → 🏄🏿‍♀️

We run a goal to obtain a (possibly empty, possibly infinite) stream of results

Goals

Goals are Python functions! 🐍

def always_pizzaᵒ(x, y):
    return eq(x, "🍕")

Goals are defined in terms of operators (e.g. eq), and goals.

Goals

When invoked, a goal returns a stream of solutions.

run(5, lambda x, y: always_pizzaᵒ(x, y))

[('🍕', _.0)]

Conjunction

Logical conjunction ("AND") combines goals.

def always_pizzaᵒ(x, y):
    return eq(x, "🍕") & eq(y, "🍺")

run(5, lambda x, y: always_pizzaᵒ(x, y))

[('🍕', '🍺')]

We've defined a relation on x and y.

Conjunction

Both sides of the conjunction must succeed for the goal to succeed.

run(5, lambda y: always_pizzaᵒ("🍍", y))

[]

No results! The goal failed.

Disjunction

Logical disjunction ("OR") also combines goals.

def always_pizzaᵒ(x, y):
    return (
        eq(x, "🍕")
        & (eq(y, "🍺") | eq (y, "🥤"))
    )

Every branch of a disjunction can contribute a solution_{(if it succeeds)}

run(5, lambda x, y: always_pizzaᵒ(x, y))

[('🍕', '🍺'), ('🍕', '🥤')]

Infinite pizza 🤯

def always_pizzaᵒ(x, y):
    return (
        eq(x, "🍕") & (eq(y, "🍺") | eq (y, "🥤"))
        | always_pizzaᵒ(x, y)
    )

Infinite pizza 😴

def always_pizzaᵒ(x, y):
    return (
        eq(x, "🍕") & (eq(y, "🍺") | eq (y, "🥤"))
        | zzz(always_pizzaᵒ, x, y)
    )

Infinite pizza 🍕

run(500, lambda x, y: always_pizzaᵒ(x, y))

[('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤'),
 ('🍕', '🍺'),
 ('🍕', '🥤')]

More examples

StreamBlock diffs

Real problem: given two StreamBlock definitions, what series of changes transforms one into the other?_{wagtail-streamfield-migration-toolkit}

StreamBlock: tree representation

Represent blocks as trees, built from linked lists.

a = parse_block(
    StreamBlock([("text", CharBlock(required=False, max_length=None))])
)
b = parse_block(
    StreamBlock([("text", CharBlock(required=True, max_length=11))])
)

_(a, b)

(("wagtail.blocks.StreamBlock"
  (("local_blocks"
    ("text"
     ("wagtail.blocks.CharBlock"
      (("required" . False) ("help_text" . None) ("max_length" . None)
       ("min_length" . None) ("validators")))))))
 ("wagtail.blocks.StreamBlock"
  (("local_blocks"
    ("text"
     ("wagtail.blocks.CharBlock"
      (("required" . True) ("help_text" . None) ("max_length" . 11)
       ("min_length" . None) ("validators"))))))))

StreamBlock diffs: example relation

def same_blockᵒ(old_block_spec, new_block_spec, path, diff):
    def _same_blockᵒ(old_type, new_type, old_spec, new_spec):
        return fresh(
            lambda: conj(
                eq(_(old_type, old_spec), old_block_spec),
                eq(_(new_type, new_spec), new_block_spec),
                eq(old_type, new_type),
                disj(
                    atomic_block_diffᵒ(old_spec, new_spec, path, diff),
                    stream_block_diffᵒ(old_block_spec, new_block_spec, path, diff),
                    list_block_diffᵒ(old_block_spec, new_block_spec, path, diff),
                ),
            )
        )
    return fresh(_same_blockᵒ)

StreamBlock diffs: getting a diff

result = run(1, lambda diff: same_blockᵒ(a, b, _("$"), diff))
diff = result[0]
diff

((("$" "text") "change_opt" "required" False True)
 (("$" "text") "change_opt" "max_length" None 11))

StreamBlock diffs: applying a diff

run(1, lambda new_block: same_blockᵒ(a, new_block, _("$"), diff))

(("wagtail.blocks.StreamBlock"
  (("local_blocks"
    ("text"
     ("wagtail.blocks.CharBlock"
      (("required" . True) ("help_text" . None) ("max_length" . 11)
       ("min_length" . None) ("validators"))))))))

StreamBlock diffs: applying a diff backwards

run(1, lambda old_block: same_blockᵒ(old_block, b, _("$"), diff))

(("wagtail.blocks.StreamBlock"
  (("local_blocks"
    ("text"
     ("wagtail.blocks.CharBlock"
      (("required" . False) ("help_text" . None) ("max_length" . None)
       ("min_length" . None) ("validators"))))))))

StreamBlock diffs: properties of relations

With one relation defined, we can do three useful things:

1. generate a diff from block a to block b
2. run the diff forwards
3. run the diff backwards

Python AST transformation

Tree representation

expr = ast.parse('f(x)', mode="eval")
expr

<ast.Expression object at 0x7fc8c13f2350>

lift_ast(expr)

("Expression"
 ("body" "Call" ("func" "Name" ("id" . "f") ("ctx" "Load"))
  ("args" ("Name" ("id" . "x") ("ctx" "Load"))) ("keywords")))

Python AST as a relation

@node("ListComp")
def list_comp_nodeᵒ(elt, generators, node):
    return conj(
        exprᵒ(elt),
        map_goal(comprehensionᵒ, generators),
    )

Program transformation: map to list comprehension

map_call = parse_expr("map(f, y)")
result = run_all(lambda x: map_to_gen_exprᵒ(map_call, "x", x))
result

[<ast.GeneratorExp object at 0x7fc8c128a5c0>]

print(ast.unparse(result[0]))

(f(x) for x in y)

Program transformation: filter to generator expression

expr = "filter(lambda x: x > 0, ints)"
result = run_all(
    lambda x: filter_to_gen_expᵒ(parse_expr(expr), "x", x)
)
unparsed = ast.unparse(result[0])
print(unparsed)

(x for x in ints if (lambda x: x > 0)(x))

list(eval(unparsed, {"ints": range(-5, 5)}))

[1, 2, 3, 4]