Previously: Rewriting the Technical Interview.

Aisha’s hands rattle you. They float gently in front of her shoulders, wrists cocked back. One sways cheerfully as she banters with the hiring manager—her lacquered nails a cyan mosaic over ochre palms. They flit, then hover momentarily as the two women arrange lunch. When the door closes, Aisha slaps her fingertips eagerly on the pine-veneer tabletop. Where have you seen them before?

But she is giggling and glad to finally meet you, and her hair bounces in loose ringlets around the shoulders of her yellow sundress, and you like her, this thirty-something engineer who has worked here three years (even if you don’t understand what it is, exactly, that she does for Mineral Analytics, Limited), who heard you were on the market, and just had to interview you personally. She tells you about the yogurt bar, and the yoga studio, and how important work-life balance is to the company. Then she asks you to balance a binary tree.

Even after all these centuries, you still have trouble grafting limbs. “I’m sorry, you’ll have to give me a moment,” you stall. “I can never keep the transformation rules straight.”

Plead with the demigoddess Andréka to intercede on your behalf.

vidrun@bamse ~> swipl

Aisha smirks. You suspect she knows something.

“Remind me, Aisha—we need to make sure that both branches have the same height? Or differ by just one?”

“At every level.” She folds her arms and offers you a break. “Would you like me to get us started?”

Release the cryptographic wards on two of your xterms, and slide the machine over.

eval_prim(Exp, _, Exp) :-
  Exp = nil ;
  Exp = [] ;
  number(Exp).

“We’ll start with terminals. Nils, empty lists, and numbers—that should be a good start, don’t you think?”

This seems reasonable enough.

“And you know we’re gonna need equality constraints. Addition too, for tree heights.”

:- use_module(library(reif)).

eval_prim([eq, A, B], Env, R) :-
  eval_exp(A, Env, ARes),
  eval_exp(B, Env, BRes),
  if_((ARes = BRes), R = true, R = nil).

eval_prim([plus, A, B], Env, R) :-
  eval_exp(A, Env, AR),
  eval_exp(B, Env, BR),
  R is AR + BR.

eval_exp(Exp, Env, R) :-
  eval_prim(Exp, Env, R), !.

Pock! She pops her tongue at the cut, startling you. Consider asking about Env, but decide against it: she clearly knows where she’s going.

Aisha gives you a very knowing look over the top of her glasses, then summons a list from the void.

eval_prim([first, List], Env, R) :-
  eval_exp(List, Env, ListR),
  if_(([] = ListR),
    R = nil,
    [R|_] = ListR).

eval_prim([rest, List], Env, R) :-
  eval_exp(List, Env, ListR),
  ((ListR = [], R = nil) ;
   (ListR = [_|R])).

eval_prim([cons, Head, Tail], Env, R) :-
  eval_exp(Head, Env, HeadR),
  eval_exp(Tail, Env, TailR),
  if_((nil = TailR), TailL = [], TailL = TailR),
  R = [HeadR | TailL].

Without moving anything else, raise a single eyebrow two centimeters.

“I’ve read your work! You couldn’t walk into a bodega without conjuring a shopping list from thin air.”

She has read you, hasn’t she?

?- eval_exp([cons, 2, [cons, 1, nil]], e{}, R).
R = [2, 1].

You’re ready to take it from here, but Aisha continues, nails clacking against the keycaps.

eval_each([], _, []).
eval_each([X | More], Env, [XR | MoreR]) :-
  eval_exp(X, Env, XR),
  eval_each(More, Env, MoreR).

“Aisha, I–”

Her hands flash and flourish, slapping out a polyrhythm you remember.

type(X, R) :-
  (atom(X),   R = atom) ;
  (number(X), R = number) ;
  ([] = X ,   R = list) ;
  (functor(X, '[|]', _),            R = list), ! ;
  (compound_name_arity(X, λ, _),    R = function), ! ;
  (compound_name_arity(X, , _),    R = macro), ! ;
  (compound_name_arity(X, Type, _), R = Type).

eval_prim([type, X], Env, R) :-
  eval_exp(X, Env, XR),
  type(XR, R).

Fy Faen! You see it now!

Snap your fingers, recalling your laptop to your hands. The instrument flies from her grasp, and you are already on your feet, anchoring yourself to the ethernet, Aisha standing in one fluid swooping motion as you cross-step back for space, one hand outstretched to seize—

—thin air.

Your laptop hovers in the air between you, screen blushing rose to iris. Aisha, yawning, checks her nails. Faint bangles of non-printable control characters encircle her wrist in glowing rings, impossible to see directly.

“Oh honey.” Her voice acquires a familiar, husky resonance.

You know her you know her you know–

She sighs in exasperation. “You’re old, not senile!”

Remember 1921: the salt-wind scoring your forehead as the bow of the Kovno cut through the cold Atlantic night. The icy pit of the Gardnos Stone, wrapped in burlap, weighing your bag as if seeking to drown the whole ship. It refused flight, warmth, comprehension. The coven had sent you in search of answers: to Antwerp, to Victorieplaats—all masonry and copper, gold figures gleaming atop the mercantile houses of the bustling diamond-hive.

You’d sought a specialist. You found Aligaz.

A eager scion of the Semien stone-mages, cast from rocky fingertips at a time of cosmopolitan awakenings, he had set up shop in an alley just south of the plaza. Géomancien, Aligaz had explained, giggling at the word, and gestured to the glittering shelves: crystals and milky stones in every color, charged by the steady glow of gaslight. All swish and charm, he had whisked the Stone from your bag and informed you, in lilting French, that you needed to lighten up. “Ces suédois!” You’d bristled at the insult… but he had, in the end, been right.

You had traded spells and languages, huddled under the rain-roaring copper roof of Aligaz’s attic. Worked together to uncover the mystery of Gardnos, and one another. Aligaz, endlessly inventive, had outmatched you at every turn: constructing puzzles within puzzles, locks which everted, became their own keys. He had delighted in your descriptions of your homeland’s fjords, and you in turn had planned to travel south with him, to see the Ethiopian landscapes he so lovingly recalled—but the coven recalled you to Skjækra. That he could stand before you now, after so many years…

“… Aisha?” You ask, tentative.

“After my aunt.” She smiles fondly.

“What a beautiful name!” It suits her well. “When did—”

“Harlem. After the war.” And here she trails off; lost, perhaps, in her own private recollection.

You are happy for Aisha, of course. To claim one’s true self is the right of all people, and the most powerful of all magics. But you have so many questions!

“What became of the Stone? How did you know? What are you doing here, of all places?”

“Vidrun, this is a geological surveying company. Of course I’m here. The question is why are you applying?”

You pause for a moment.

Why are you here?

“You summoned me!”

“I didn’t know for sure,” she admits. “But rumors spread, and your style is distinctive. How could I pass over the chance to challenge you once more?”

Now the meaning of her spell becomes clear: a trap laid not to ensnare, but to evince. She has offered you a gift. Return the laptop to her, and accept the invitation with grace.

bind(K, V, Env, Env2) :-
  atom(K),
  Env2 = Env.put(K, V).

“I bind you, Vidrun,” she intones. Her voice now carries the weight of the Semien, of the Alps, of the Sierra Nevada. A century has grounded her.

“I bind you head and tail.”

bind([], _, Env, Env).
bind([K|Ks], Vs, Env, Env3) :-
  (K = &(K2),
   bind(K2, Vs, Env, Env3), !) ;
  ([] = Vs,
   bind(K, nil, Env, Env2),
   bind(Ks, [], Env2, Env3));
  ([V1|V1s] = Vs,
   bind(K,  V1, Env, Env2),
   bind(Ks, V1s, Env2, Env3)).

Your breath catches in your throat.

“You shall see only that which is shown,” she continues.

eval_var(Var, Env, R) :-
  atom(Var),
  get_dict(Var, Env, R).

“You may speak without speaking,”

eval_prim([quote, R], _, R).

“And within these bounds, you may choose your own path.”

eval_prim([cond], _Env, nil).
eval_prim([cond, Default], Env, R) :-
  eval_exp(Default, Env, R).
eval_prim([cond, Test, Branch | More], Env, R) :-
  eval_exp(Test, Env, TestR),
  if_((nil = TestR),
    eval_prim([cond | More], Env, R),
    eval_exp(Branch, Env, R)).

A Lisp, then. Murmuring softly, you offer a prayer to McCarthy. Hopefully Aisha does not expect you to reinvent lambdas from scratch.

“What you let, will become.”

eval_prim([let, [], Body], Env, R) :-
  eval_exp(Body, Env, R).
eval_prim([let, [K, V | More], Body], Env, R) :-
  eval_exp(V, Env, VR),
  bind(K, VR, Env, Env2),
  eval_prim([let, More, Body], Env2, R).

Well, that’s something, at least. Serial assignment, too—a luxury. But Aisha is not finished. She clacks her heels firmly onto the industrially-sealed concrete, and opens her arms wide. Her palms are ruddy laterite, her upturned eyes glinting magnetite under halogen stars.

evoke(Vars, Args, Body, Env, R) :-
  bind(Vars, Args, Env, Env2),
  eval_exp(Body, Env2, R).

eval_application([Fun | Args], Env, R) :-
  eval_exp(Fun, Env, FunR),
  FunR = λ(Vars, Body, Env2),
  eval_each(Args, Env, ArgsR),
  evoke(Vars, ArgsR, Body, Env2, R).

The Church. The lambda calculus. The gay agenda. It has known a thousand names, a thousand forms. Aisha slams her palms together, and with the crash of mountains, summons the thousandth-and-first.

eval_prim([lambda, Args, Body], Env, R) :-
  R = λ(Args, Body, Env.put(recur, R)).

The conference room twists, folds somehow. Outside, the rows of desks and office furniture rush away to the horizon, replaced by a featureless expanse of evenly-lit pine. On the tabletop, a miniature cube of glass and concrete inflates from nothing to a tiny, modernist dollhouse. You lean over to look inside, notice the light outside the conference room abruptly dim, and think better of it.

eval_exp(Exp, Env, R) :-
  eval_var(Exp, Env, R), ! ;
  eval_prim(Exp, Env, R), ! ;
  eval_application(Exp, Env, R), !.

Aisha takes a deep breath and regains her composure. You sense her spell is near complete.

Whisper softly, so as not to disturb her work. “Macros?”

She glares sidelong, eyes wide. “Really?”

“It’ll be fun.”

eval_prim([gensym, Prefix], _Env, R) :-
  atom_concat(Prefix, '__auto__', Sym),
  gensym(Sym, R).

eval_prim([macro, Args, Body], Env, R) :-
  R = (Args, Body, Env).

eval_application([Fun | Args], Env, R) :-
  eval_exp(Fun, Env, FunR),
  ((FunR = λ(Vars, Body, Env2),
    eval_each(Args, Env, ArgsR),
    evoke(Vars, ArgsR, Body, Env2, R)) ;
  (FunR = (Vars, Body, Env2),
     evoke(Vars, Args, Body, Env2, Code),
     eval_exp(Code, Env, R))).

“One more thing,” you request. “Some kind of product type.”

“Ma’am, this is a Wendy’s.”

“Do you really want to watch me reinvent a dynamic type system on top of bare lists?”

Aisha considers the possibility—somewhat sadistically, you think—but this is not that kind of interview.

“Fine. But that’s ALL you’re getting.”

eval_prim([struct, Type | Fields], Env, R) :-
  eval_each(Fields, Env, FieldsR),
  compound_name_arguments(R, Type, FieldsR).

eval_prim([destruct, Type, Struct], Env, R) :-
  eval_exp(Struct, Env, StructR),
  compound_name_arguments(StructR, Type, R).

Your hair charges with static as Aisha seals the spell. Her nails flare in the light, leaving cyan trails in the air above the keyboard. As she executes the final command, you feel your connection with Andréka severed. You are locked in Aisha’s calculus now.

“I knew exactly where you were going with this, Vidrun. You couldn’t remember how to balance a binary tree, so you thought you’d define the transformational invariants and have Prolog solve them for you.”

“So you’re trapping me in a Lisp instead.”

“Would you have preferred an Algolem?” Aisha smirks. You would not.

Very well. Sprinkle salt, as is tradition, in the protective form of two parentheses. No—you wipe the salt clear—square brackets. Test the forms of this new plane.

?- eval_exp([let, [list, [lambda, [&(args)], args]], [list, 1, 2, 3]], e{}, R).
R = [1, 2, 3].

It’s not much, but it’s a start. Aisha watches you expectantly; you need to do something. Stall for time by summoning an algebra.

  and, [macro, [a, b],
  [list, [quote, cond], a, b]],

  or, [macro, [a, b],
    [let, [a_, [gensym, a]],
      [list, [quote, let],
             [list, a_, a],
             [cond, a_, a_, b]]]],

  not, [lambda, [x], [cond, x, nil, [quote, true]]],

Aisha makes a show of yawning. Bore her with type predicates.

  is_null, [lambda, [x],
    [or, [eq, x, []],
         [eq, x, nil]]],
  
  is_list, [lambda, [x],
    [eq, [type, x], [quote, list]]],

  is_pair, [lambda, [x],
    [and, [not, [is_null, x]],
          [is_list, x]]],

  is_fn, [lambda, [x],
    [eq, [type, x], [quote, function]]],

You think you’re getting the hang of this—though you haven’t used your comma key this much in years. It’s all so excitingly verbose.

  second, [lambda, [coll], [first, [rest, coll]]],

  map, [lambda, [f, coll],
    [cond, [is_null, coll],
      [],
      [cons, [f, [first, coll]],
             [recur, f, [rest, coll]]]]],

  find, [lambda, [f, coll],
    [cond, [is_pair, coll],
      [let, [x, [first, coll]],
        [cond, [f, x],
          x,
          [recur, f, [rest, coll]]]]]],

  fold, [lambda, [f, init, coll],
    [cond, [is_null, coll], init,
           [recur, f, [f, init, [first, coll]], [rest, coll]]]],

  rev, [lambda, [coll],
    [fold, [lambda, [list, elem], [cons, elem, list]], [], coll]],
[rev, [list, 1,2,3]]
R = [3, 2, 1].

Smile, wistfully. That had been a good interview.

  syntax_quote_fn, [lambda, [expr],
    [cond, [is_null, expr], expr,
           [is_list, expr],
           [let, [f, [first, expr]],
             [cond, [eq, f, [quote, unquote]],
                    [second, expr],
                    [cons, [quote, list],
                           [map, recur, expr]]]],
           [list, [quote, quote], expr]]],
  syntax_quote, [macro, [expr], [syntax_quote_fn, expr]],

“Honestly!” Aisha mutters. “I don’t know what you wanted macros for in the first place. Is this really necessary for balancing a tree?”

Keep your expression as enigmatic as possible. She may have cut you off from the Goddess Andréka, but you can will your own deities into existence.

  lvar,     [lambda, [num], [struct, lvar, num]],
  is_lvar,  [lambda, [x], [eq, [quote, lvar], [type, x]]],
  lvar_num, [lambda, [x], [first, [destruct, lvar, x]]],

Aisha’s jaw drops as she grasps your scheme. “You have got to be kidding.”

“Kiselyov, Friedman, Byrd”, you incant. “I call upon you, triune, though you have never dwelt within these forms. May you walk this plane as well!”

  walk, [lambda, [u, subs],
    [let, [pr, [and, [is_lvar, u],
                     [find, [lambda, [v],
                              [eq, u, [first, v]]],
                            subs]]],
      [cond, pr,
             [recur, [rest, pr], subs],
             u]]],

“May all merge within your reasoned embrace!”

  ext_s, [lambda, [x, v, subs],
    [cons, [cons, x, v], subs]],
  unify, [lambda, [u, v, subs],
    [let, [u, [walk, u, subs],
           v, [walk, v, subs]],
      [cond, [eq, u, v], subs,

             [is_lvar, u], [ext_s, u, v, subs],
             [is_lvar, v], [ext_s, v, u, subs],

             [and, [is_pair, u], [is_pair, v]],
             [let, [subs, [recur, [first, u], [first, v], subs]],
               [and, subs, [recur, [rest, u], [rest, v], subs]]]]]],

Aisha locks eyes with you. Inside each of you, something shifts, merges, becomes bound.

  mzero, [],

“M’Zero,” she quips, and you share a giggle.

“Absolute unit,” you respond.

  unit, [lambda, [state],
    [cons, state, mzero]],

Demand equality. Some would call this a constraint, but you know it to be foundational.

  eql, [lambda, [u, v],
    [lambda, [st],
      [let, [subs, [unify, u, v, [first, st]]],
        [cond, subs,
          [unit, [cons, subs, [rest, st]]],
          mzero]]]],

“May this space be open to newcomers,” you declare.

  call_fresh, [lambda, [f],
    [lambda, [st],
      [let, [c, [rest, st]],
        [[f, [lvar, c]],
         [cons, [first, st], [plus, 1, c]]]]]],

“And may their futures weave a beautiful tapestry.” You forsee threads of execution racing ahead, taking turns, alternating and combining.

  mplus, [lambda, [a, b],
    [let, [mplus, recur],
      [cond, [is_null, a], b,  
             [is_fn, a], [lambda, [], [mplus, b, [a]]],
             [cons, [first, a], [mplus, [rest, a], b]]]]],

  bind, [lambda, [stream, goal],
    [let, [bind, recur],
      [cond, [is_null, stream], mzero,
             [is_fn, stream], [lambda, [], [bind, [stream], goal]],
             [mplus, [goal, [first, stream]],
                     [bind, [rest, stream], goal]]]]],

Imbue the triune with its own algebra.

  disj, [lambda, [g1, g2],
    [lambda, [state],
      [mplus, [g1, state], [g2, state]]]],

  conj, [lambda, [g1, g2],
    [lambda, [state],
      [bind, [g1, state], g2]]]

Moving carefully, you follow a thread of that tapestry to its first few knots.

  pull, [lambda, [stream],
    [cond, [is_fn, stream],
      [recur, [stream]],
      stream]],

  take, [lambda, [n, stream],
    [cond, [eq, 0, n],
      [],
      [let, [stream, [pull, stream],
             state,  [first, stream]],
        [cond, state,
               [cons, state, [recur, [plus, n, -1], [rest, stream]]],
               []]]]],

  run_raw, [lambda, [n, goal],
    [take, n, [goal, [cons, [], 0]]]],

The work complete, you let go a sigh. Your godhead takes its first tottering steps.

?- eval([run_raw, 3, [call_fresh, [lambda, [x], [disj, [eql, x, [quote, aisha]], [eql, x, [quote, vidrun]]]]]],
R = [[[[lvar(0)|aisha]]|1], [[[lvar(0)|vidrun]]|1]].

“You absolute madwoman,” Aisha chortles. “You can’t remember how to balance a binary tree, but you memorized µKanren?”

“It comes in handy!” You stammer. “And honestly, it’s shorter.” Offer her a reifier by way of apology.

“Fine. Fine!” Aisha throws up her hands in mock exasperation. “I’ve let you get away with it this far!”

  walkr, [lambda, [v, subs],
    [let, [v,     [walk, v, subs],
           walkr, recur,
           w,     [lambda, [v2], [walkr, v2, subs]]],
      [cond, [is_lvar, v], v,
             [is_pair, v], [cons, [w, [first, v]],
                                  [w, [rest, v]]],
             v]]],

  reify, [lambda, [states],
    [map, [lambda, [state],
            [walkr, [lvar, 0], [first, state]]],
          states]]

“Only with respect to the first variable,” you explain. “But it still makes things easier to read.”

eval([reify, [run_raw, 3, [call_fresh, [lambda, [x], [disj, [eql, x, [quote,
aisha]], [eql, x, [quote, vidrun]]]]]]], R).
R = [aisha, vidrun].

Aisha has the look of a woman who has realized, six hours into her shift, that she has left the oven on. “That’s why you wanted macros. You wanted syntax for this rickety-ass interpreter.”

Reward her insight by entering the metatrance of creation, and let the forms spill from your fingertips.

  zzz, [macro, [g],
    [let, [state_, [gensym, state]],
      [syntax_quote,
        [lambda, [[unquote, state_]],
          [lambda, [],
            [[unquote, g], [unquote, state_]]]]]]],

  conjall, [macro, [&(gs)],
    [let, [[g, &(gs)], [rev, gs]],
      [fold, [lambda, [form, goal],
                     [syntax_quote,
                       [conj, [zzz, [unquote, goal]], [unquote, form]]]],
                   [list, [quote, zzz], g],
                   gs]]],

  disjall, [macro, [&(gs)],
    [let, [[g, &(gs)], [rev, gs]],
      [fold, [lambda, [form, goal],
               [syntax_quote,
                 [disj, [zzz, [unquote, goal]], [unquote, form]]]],
             g,
             gs]]],

  conde, [macro, [&(clauses)],
     [cons, [quote, disjall],
            [map, [lambda, [goals],
                    [cons, [quote, conjall], goals]],
                  clauses]]],

  fresh, [macro, [vars, &(goals)],
     [fold, [lambda, [form, var],
              [syntax_quote,
                [call_fresh, [lambda, [[unquote, var]],
                               [unquote, form]]]]],
            [cons, [quote, conjall], goals],
            [rev, vars]]],

  run, [macro, [n, vars, &(goals)],
    [syntax_quote,
      [reify, [run_raw, [unquote, n],
                        [unquote,
                          [cons, [quote, fresh],
                                 [cons, vars, goals]]]]]]]

Crack your knuckles, and enjoy the series of pops which fizzle from somewhere under your keyboard. “Would you like to do the honors?”

Aisha, half-amused, half exasperated, draws a shining hair from her scalp. Fingers deft, she ties a knot in it for zero.

  succ, [lambda, [n], [cons, [quote, 'S'], n]],
  n0, [list, 0],
  succo, [lambda, [n, next], [eql, [succ, n], next]],

You draw one of your own, and align them, side by side.

  lesso, [lambda, [lesser, greater],
    [let, [lesso, recur],
      [fresh, [g],
        [succo, g, greater],
        [conde, [[eql, lesser, g]],
                [[lesso, lesser, g]]]]]],

  maxo, [lambda, [a, b, max],
    [conde, [[eql, a, b],   [eql, max, a]],
            [[lesso, a, b], [eql, max, b]],
            [[lesso, b, a], [eql, max, a]]]],

  approxo, [lambda, [a, b],
    [conde, [[eql, a, b]],
            [[succo, a, b]],
            [[succo, b, a]]]],

Aisha reaches into her purse, and withdraws a single gleaming seed. This she sets gently upon the table, and waits for you to draw it to fruition.

  leaf, [lambda, [x],
    [list, [quote, leaf], x]],

  branch, [lambda, [left, right],
    [list, [quote, branch], left, right]],

A maple tree in miniature, no more than 4 inches high, rises from the tabletop. Outside, in the vast expanse of tabletop, its twin—writ large—swells to full size.

Aisha recognizes the form you have chosen, and raises a spell of translation around it.

  tree, [lambda, [t],
    [cond, [is_list, t],
           [let, [[left, right], t],
             [branch, [recur, left], [recur, right]]],

           [leaf, t]]],

  untree, [lambda, [[type, a, b]],
    [cond, [eq, type, [quote, branch]], [list, [recur, a], [recur, b]],
           [eq, type, [quote, leaf]],   a]],

With a flick of your hands, the tree shimmers, reforms.

[tree, [quote, [1, [2, 3]]]]
R = [branch, [leaf, 1], [branch, [leaf, 2], [leaf, 3]]].

You measure along each leaf, each branch, and find the height thereof.

  heighto, [lambda, [t, h],
    [let, [heighto, recur],
      [conde, [[fresh, [x],
                 [eql, t, [leaf, x]],
                 [eql, h, n0]]],
              [[fresh, [left, right, left_height, right_height, max_height],
                 [eql, t, [branch, left, right]],
                 [heighto, left, left_height],
                 [heighto, right, right_height],
                 [maxo, left_height, right_height, max_height],
                 [succo, max_height, h]]]]]],

Pause a moment, and look to Aisha. A balanced tree: each branch of roughly the same height. Each branch, in turn, a balanced tree itself. Speaking slowly, then faster, in unison, recite:

  balancedo, [lambda, [t, h],
    [let, [balancedo, recur],
      [conde, [[fresh, [x], [eql, t, [leaf, x]]]],
              [[fresh, [left, right, left_height, right_height],
                 [eql, t, [branch, left, right]],
                 [balancedo, left],
                 [balancedo, right],
                 [heighto, left, left_height],
                 [heighto, right, right_height],
                 [approxo, left_height, right_height]]]]]],

With all the delicacy you can muster, you peel boughs from trunks, rearrange, then press the limbs gently together. Aisha leans in and blows; the warmth of her breath speeding the healing process.

  rot_lefto, [lambda, [t1, t2],
    [fresh, [a, b, c],
      [eql, t1, [branch, a, [branch, b, c]]],
      [eql, t2, [branch, [branch, a, b], c]]]],

Aisha folds her hands together, whispers an incantation, and unfolds them. The maple peels apart into mirrored copies.

  rot_botho, [lambda, [t1, t2],
    [conde, [[rot_lefto, t1, t2]],
            [[rot_lefto, t2, t1]]]],

Following her lead, you thrust your hands forth and split your fingers in twos, then fours. The tree flickers, expanding into a small forest of copies–each different in exactly one way.

  roto, [lambda, [t1, t2],
    [let, [roto, recur],
      [conde, [[rot_botho, t1, t2]],
              [[fresh, [t1l, t1r, t2l, t2r],
                 [eql, t1, [branch, t1l, t1r]],
                 [eql, t2, [branch, t2l, t2r]],
                 [conde,
                   [[eql, t1r, t2r], [roto, t1l, t2l]],
                   [[eql, t1l, t2l], [roto, t1r, t2r]]]]]]]],

Aisha snaps, and with a thwap, unfurls a ludicrously oversized hand-fan from thin air. You ask her where she summoned it from, and how did she ever get Turing to sign it—but she simply bats her eyes and fans herself, looking incredibly smug.

  rotso, [lambda, [t1, t2],
    [let, [rotso, recur],
      [conde, [[eql, t1, t2]],
              [[fresh, [t],
                 [roto, t1, t],   
                 [rotso, t, t2]]]]]],

The tabletop is filled with trees; outside the conference room, an infinite forest of golden leaves shimmers. Aisha’s fan waves, and a thousand branches whisper in wind-dappled light.

When she refurls the fan, the forest folds with it. Only a solitary tree remains.

It is an act of extraordinary beauty, and for a moment, you are back in the Victorieplaats attic: sunset cast through time-warbled windows, each amber shaft holding sparkling motes of dust which blaze into light, drift briefly, and then go dim again: not lost, merely out of view, and Aisha is whispering an incantation to you, her words unfolding a map within a map within your mind, and you wonder, had you not been recalled, what more you might have become…

“Vidrun. Almost there.”

You take her offered hand in yours, and voices evenly matched, complete the spell.

  balanceo, [lambda, [tree, balanced],
    [conde, [[rotso, tree, balanced],
             [balancedo, balanced]]]]

Measuring carefully and whispering to herself, Aisha encodes the tree in front of you, and asks for its balanced form:

[map, untree, [run, 1, [t], [balanceo, [tree, [quote, [[0,1],[[2,[3,4]],5]]]], t]]]
R = [[[[0, 1], 2], [[3, 4], 5]]].

The tree shifts, blurs, and for an instant you perceive a forest of its balanced siblings, each one possible, but this one yours, and there it is: golden leaves arranged exactly as they were before, but supported by new, more even branches. As her spell unwinds, and the conference room re-attaches to reality, Aisha beams.

“I knew you couldn’t do anything the easy way.”

“Never have,” you admit. “Thank you, Aisha.”

“Any time,” she smiles, and from the tabletop, into your outstretched palms, delivers you a gleaming maple seed.


With sincerest thanks to Taber Bain, Zyle Cook, Brad Greenlee, Coda Hale, Duretti Hirpa, Moishe Lettvin, Dan Mess, Kit Patella, and Emily St, who contributed research, story suggestions, and feedback on initial drafts.

This work was inspired by Andréka and Németi’s 1978 The Generalized Completeness of Horn Predicate Logic as a Programming Language, which shows that logic programs are Turing-complete, as well as McCarthy’s 1955 Lisp paper which defines a Lisp evaluator (including recursive lambdas!) in terms of a handful of basic functions: car, cdr, cons, cond, and so on. It also draws on Steele Jr & Sussman’s The Art of the Interpreter. I designed several Prolog metacircular interpreters based on both of these papers, but ultimately wrote the (much more complex) interpreter here in search of concision and execution speed. The µKanren implementation is directly taken from µKanren: A Minimal Functional Core for Relational Programming, by Hemann & Friedman, though Vidrun invokes Friedman, Byrd, and Kiselyov for their work on The Reasoned Schemer. An earlier version of this work followed Byrd, Holk, and Friedman in using miniKanren to generate quines: Vidrun was to escape a trap by constructing interpreters which interpreted themselves. This approach seemed too derivative, and balancing a binary tree was an interview question which I personally bombed in 2010; it felt nice to revisit the problem with Aisha & Vidrun at the helm.

You can find a fully commented and expanded version of Aisha & Vidrun’s program here. This version includes (do ...) expressions, side effects, stacktraces, additional literals, eval, and a partial dynamic type system. In addition to balancing binary trees, it includes a tiny lambda-calculus interpreter: a sort of lisp-in-minikanren-in-lisp-in-prolog.

Doga
Doga on

Honestly, I don’t even understand 95% of what’s going on here but I still love this series so much. I can only imagine how amazed I would be if I could fully comprehend the insanity happening here. Great work as always!

Spock
Spock on

Ya know, Christopher Nolan might be interested in the rights to turn this one into a movie…

Seriously though, amazing work.

Manu Ebert

Reminds me of my college class when my AI prof (back then it was all GofAI) implemented Lisp in Prolog in on one blackboard and then “ran” it while using a second blackboard to draw and update a memory register in real time to demonstrate how it works. Most mind-bending lecture I’ve ever seen.

Proof: https://github.com/maebert/prolog_puzzles#prolog-puzzles-for-fun-and-profit-mostly-fun

Richard Barrell

Until she got to the kanren implementation, I was half expecting to see pi-calculus and a large chunk of an Erlang interpreter to pop out.

Thank you for writing this, it’s beautiful and you’ve made my day markedly better. ♥️

Will Byrd

This made my day. Thank you!

We’ve gotten more sophisticated about writing relational LISP/Scheme interpreters since the 2012 Quines paper–for example, [0]. We can even do a decent Lisp-within-LISP-within-miniKanren. However, I’ve never been happy with our efforts at miniKanren-within-miniKanren, or miniKanren-within-LISP-within-miniKanren. Maybe your code can serve as an inspiration to do better.

[0] https://dl.acm.org/doi/10.1145/3110252 and http://io.livecode.ch/learn/gregr/icfp2017-artifact-auas7pp

kora
kora on

Gosh, this was (as usual) really wonderful, (and thanks for including trans characters!!) I’m gonna be untangling this for a while - thank you for bringing some joy and magic to CS!

Aphyr on

This made my day. Thank you!

Ahhhh I never imagined you’d actually see this! I’m glad you liked it! Your papers have been truly inspirational reading. :-)

Aphyr
deosjr
deosjr on

As a programmer whose first love was Prolog, this is absolutely beautiful. It has finally prompted me to dive head-first into uKanren and related languages. I should’ve followed up when I first saw it years ago. Thank you for pushing me onwards :)

RPS

A smoldering pseudo-romance with sex, intrigue and maple seeds. Perfect

Peter
Peter on

Good story, nice hack, but I don’t see how the search strategy defined by rotso doesn’t just go in infinite loops in the search space…

Aphyr on

I don’t see how the search strategy defined by rotso doesn’t just go in infinite loops in the search space

It actually is infinite! This works because of the pair of control-flow operators mplus and bind, (plus zzz) which turn what would be an infinite loop in an eager language into a lazily evaluated search of the state space. And indeed, if we were to realize any of these results eagerly, we would get stuck in loops. It only works because the entire search is encoded in this infinite lazy tree, and we eventually (through the mplus alternator) wind up exploring the non-looping branches enough to find a solution.

Aphyr
Kristof
Kristof on

Oh man, this brings back memories!

In 2008 I attended on our weekly philosophy and logic seminar Andréka & Németi’s talks on the “chicken and egg problem of set theory and logic”. Mostly it flew over my head, but I remember her as a really friendly goddess. Always helping, always smiling, and proving any new set theory thought up on the seminar to be equivalent to some already known esoteric set theory in 5 minutes.

Dave
Dave on

I laughed out loud as each part was revealed and I started to see where it was going. Best line: “You think you’re getting the hang of this—though you haven’t used your comma key this much in years.”

Arthur
Arthur on

This is amazing! I actually stumbled on this in the wild while taking a class with Dan Friedman. We just did miniKanren in racket, so this is eerily familiar.

silas
silas on

why is if_/3 used instead of the standard Prolog -> if?

Aphyr on

why is if_/3 used instead of the standard Prolog -> if?

It’s entirely possible I messed this up–I’m only a Prolog beginner. I had issues with exhaustiveness and only sort of understand cuts, and it seemed (to my entirely unexperienced eyes) like what I actually wanted was the reified if. I really do think a Prolog expert could do this better!

Aphyr
Kasran

i’ve just read through all the vidrun stories, and they’re my most favorite artifacts of computer science fiction by a long shot. 100% kudos for the excellent work; if you ever write more vidrun stuff, i will eagerly read it!

johno

I was sent “Hexing” and couldn’t stop reading until I got to the end of the series, other work be damned! This whole series is incredible, even if I gave up on actually parsing most of the code so that I could keep enjoying the writing. Recursion in the room on this one was a really nice touch.

If you ever find the time & inclination to write more, count one more loyal reader! I wanted to send you money for creating this, but there appears to be no path for that. Thank you for sharing :)

Aphyr on

Thanks, all of you. I really appreciate it. :-)

Aphyr
Anonymous Coward
Anonymous Coward on

I do not normally read your blog.

Anytime I see there’s a new one of these, I come running.

Fred Ross

This has preemptively one upped my plans for writing a romance novel centered around Bessel functions. And I haven’t laughed this hard in years.

Danielle Church

Oops, first line got cut off there, trying again:

My wife sent me to the first in this series, but I squealed when I finally got to this one and I saw what interpreter she was using! My Prolog isn’t that strong, but since you’ll nonetheless find my name all over the swipl codebase, I like to imagine that this trans enby got to help, in some small way, with Vidrun’s triumph here 😍

I’ll be sending this onward to Jan, of course, but I’ll be somewhat shocked if he hasn’t seen it already - this whole series is BRILLIANT 😂 Thank you so, so very much for the read!

One question - is there a bug in lvar_num? It calls out to destruct with foo as the type; that should be lvar, yes?

Aphyr on

… you’ll nonetheless find my name all over the swipl codebase, I like to imagine that this trans enby got to help, in some small way, with Vidrun’s triumph here 😍

Oh my gosh, I’m delighted to find out about this! I’m sure your work contributed in some way. I’d never really used Prolog (I mean, I’d done some basics, but nothing nontrivial) before learning swipl to write this piece, and it was truly a delight. Thank you for helping make this possible!

One question - is there a bug in lvar_num? It calls out to destruct with foo as the type; that should be lvar, yes?

Oh, uhh…. wow, no, you’re totally right. That’s in my original source too–I think I sketched it out for a more full-featured kanren but never actually used it, so the bug never showed up. Good catch!

Aphyr
aw

That’s a nice take on fairy tales.

Now the question is how to bewitch parents into reading these to their kids.

Sadly precious few ever learn that the Arts even exist, much less learn to practice them.

Adam Thornton
Adam Thornton on

This is one of the few love stories that reliably makes me tear up every time I revisit it, which is a couple times a year. The only thing that immediately comes to mind as a comparison is “Chip Crockett’s Christmas Carol.”

Also, the puns and multiple-entendres in this story are just so magnificent.

Thank you.

Post a Comment

Comments are moderated. Links have nofollow. Seriously, spammers, give it a rest.

Please avoid writing anything here unless you're a computer. This is also a trap:

Supports Github-flavored Markdown, including [links](http://foo.com/), *emphasis*, _underline_, `code`, and > blockquotes. Use ```clj on its own line to start an (e.g.) Clojure code block, and ``` to end the block.