A Jupyter and a Caderno kernel for combinatory logic (combinator calculus): S/K/I, BCKW, and the Smullyan aviary (Bluebird, Cardinal, Mockingbird, Phoenix, Psi, Vireo, the once- and twice-removed permuting birds, and more), evaluated under normal-order (leftmost-outermost, lazy) reduction to full normal form.
K ▲ (M M)
▲ [1 step]
M M (the classic non-terminating self-application) is never touched --
that's normal order's laziness in action. See SPEC.md for the full
design and demo.ipynb for a guided tour, including a computational
proof-sketch of Smullyan's Mockingbird fondness theorem.
Requires Python >= 3.10.
pip install aviary-kernel
python -m aviary_kernel.install --user # or --prefix /path/to/envOr from a checkout, for development:
python3 -m venv .venv && source .venv/bin/activate
pip install -e .
python -m aviary_kernel.install --prefix .venvThis registers a kernelspec named aviary, displayed as
"Aviary (Combinator Calculus)" in Jupyter frontends. Then:
jupyter notebook demo.ipynb # open the demo
jupyter console --kernel aviary # or drop into a REPL(--user installs into your per-user Jupyter kernel directory;
--prefix .venv installs into the active virtualenv instead, which is
handy for local development without touching your global Jupyter
config.)
A cell is a sequence of lines; each non-empty line is one statement: a
magic (%name ...), a definition (Name := expr or
Name v1 v2 -> expr), or an expression. # starts a comment.
Application is left-associative and implicit -- S K K means
((S K) K). Parentheses group; S K (K I) differs from S (K (K I)).
Any built-in bird, or arbitrary Unicode atom (▲, 🟢, foo_bar), can
appear free:
B ▲ 🟢 (K ◆ ●)
▲ (🟢 ◆) [2 steps]
Names like Q1/Q₁, W'/W′/W¹, and E^/Ê are the same bird
under Unicode normalization (subscript digits, primes, superscript one)
and explicit ASCII aliases; %ascii on/off picks which script output
uses.
🟢 x y z -> x (z y) # rule (a new combinator of arity 3)
Theta := U U # alias (already preloaded, for reference)
Rules can be recursive (the name may appear in its own body -- that's
how you'd hand-roll a sage bird); recursive definitions reduce fine but
can't be basis-expanded to a finite S/K/I term (%ski raises an error
explaining why, and suggests routing through Y/Θ instead). Redefining
a built-in is an error; redefining a user definition replaces it.
%undef Name removes a user definition; %defs lists them all.
| Magic | Effect |
|---|---|
%trace expr |
step-by-step reduction trace |
%whnf expr |
reduce to weak head normal form only |
%ski expr / %sk expr |
basis-expand to S/K/I (or strict S/K); does not reduce |
%fuel N |
set the step budget for the session (bare form prints it) |
%size N |
set the term-size guard (bare form prints it) |
%birds |
table of the whole registry |
%whatis X |
one bird/definition's name(s), arity, rule, λ-form, and S/K/I form |
%defs |
list user definitions |
%undef X |
remove a user definition |
%ascii on|off |
toggle Q1 vs Q₁-style output |
Reduction is fuel-bounded (10 000 steps and 100 000 atoms by default);
running out is a warning, not an error -- you get the partial term
back and can raise the budget with %fuel/%size and try again:
M M
M M [10000 steps]
⚠ no normal form after 10000 steps (fuel exhausted); term size 3
Bracket abstraction is derived, not hand-copied. Every non-recursive bird's S/K/I form comes from Curry's bracket-abstraction algorithm applied to its rule, on demand:
%ski Q₁
S (S (K S) (S (K K) (S (K S) K))) (K (S (K (S I)) K))
%trace shows normal order at work, including descent into stuck
arguments once the head sticks:
%trace Φ B C K x y
0 Φ B C K x y
Φ 1 B (C x) (K x) y
B 2 C x (K x y)
K 3 C x x
aviary_kernel/
terms.py Term model (Atom | App), pretty-printer
parser.py lexer + parser -> Term
birds.py the bird registry (verified against two independent sources; see below)
reduce.py normal-order reducer: iterative, fuel/size/interrupt-checked
abstraction.py bracket abstraction -> S/K/I (and S/K)
magics.py %-command dispatch
kernel.py AviaryKernel(ipykernel.kernelbase.Kernel)
install.py `python -m aviary_kernel.install` writes the kernelspec
kernelspec/ kernel.json
tests/ pytest suite (parser, birds, reduce, abstraction, kernel end-to-end)
demo.ipynb living documentation / acceptance demo
SPEC.md the full design spec
pip install -e '.[test]'
pytest # full suite
python -m aviary_kernel.install --prefix .venv # register the kernel into this venvThe bird registry (birds.py) was cross-checked row by row against the
Wolfram Data Repository's Combinator Birds dataset (via its own cited
primary source, Chris Rathman's chart, fetched through the Wayback
Machine) and combinatorylogic.com's table -- see the header of
tests/fixtures_birds.py for the two source discrepancies that surfaced
during verification (and how they were resolved) and tests/test_birds.py
for the resulting behavioral-equivalence oracles.
Aviary also ships as desk/, a self-contained Urbit desk: the %aviary
/lib/shoe agent is a sibling Hoon port of this same combinator-calculus
engine (same language, same semantics -- SPEC.md §§3-8), usable both
interactively from a terminal |shoe session and as a
caderno kernel. See
SPEC-DESK.md for the full desk-level spec.
Magics: %ski, %sk, %fuel, %defs, %undef (SPEC-DESK.md's v1
scope), plus all six originally-deferred-to-v1.1 magics, now implemented:
%trace, %whnf, %size, %ascii, %birds, and
%whatis -- full magic-level parity with the Python kernel (SPEC.md
§9's protocol-level surface -- do_inspect/do_interrupt have no
equivalent in the shoe/sole kernel contract this desk builds on, since
Gall pokes are synchronous and %whatis already covers do_inspect's
job). %trace's output format matches the Python
kernel's exactly: each line is the contracted combinator's canonical name
(not its Unicode display form) left-padded to 4 columns, the step number
right-padded to 4 columns, two spaces, then the term -- e.g. %trace K x1 (M x1) prints
0 K x1 (M x1)
K 1 x1
Traces obey the session's fuel the same as a plain expression (a fuel/size warning line, never an error) and elide the middle beyond 200 lines when running under the default (unraised) fuel.
%whnf expr (SPEC.md §6.1/§9) reduces only to weak head normal form --
it contracts head-position redexes but never descends into arguments to
normalize them, so %whnf B x1 (M x2) prints B x1 (M x2) [whnf, 0 steps] (stuck: B needs 3 args, has 2) where the plain expression B x1 (M x2) would print B x1 (x2 x2) [1 step] (arguments get normalized
once the head is stuck). Matching the Python reference exactly, %whnf's
status is always whnf (never normal, even at 0 steps) and it prints
only the one result line -- no separate "⚠" warning line on fuel/size
exhaustion, unlike a plain expression or %trace.
%size N (SPEC.md §9) is %fuel's sibling: it gets/sets the session's
max_size term-size ceiling (previously a fixed 100,000-atom constant,
now per-session state, same as fuel).
%ascii on|off (SPEC.md §9) toggles the session's display script for
bird names whose canonical name differs from their preferred display
form -- e.g. Q1 prints as Q₁ by default (%ascii off) and as Q1
under %ascii on.
%birds (SPEC.md §9) prints the whole registry, one fixed-width row per
bird, sorted by canonical name -- unlike the Python reference (which also
emits a text/markdown table for rich frontends), this is plain text
only, since the shoe/sole kernel contract has no rich-display channel;
it's the same information, just the one rendering the contract can
actually carry.
%whatis X (SPEC.md §9) prints a four-line card for a bird (by
canonical name or alias) or a user/built-in definition (including Θ,
which is preloaded exactly as if Θ := U U had been typed, per
SPEC.md §5.2): the name(s)/kind/arity header, the rule, the λ-form, and
the S/K/I expansion (or an (unexpandable: ...) fallback for a
recursive user rule, same wording %ski itself would error with).
Tab completion: app/aviary.hoon implements +tab-list for real
(every bird name and alias, every magic name, and the session's own
user definitions, each with a one-line detail) -- this is Aviary's half
of SPEC-DESK.md §1/§10's deferred "completion/tab-list beyond shoe's
default," reusing the vendored lib/language-server-complete.hoon
prefix-matching machinery /lib/shoe's own +tab arm already calls for
any real sole session (terminal |shoe, or |dojo/linked to one).
Whether a caderno notebook cell ever exercises this is a separate,
Caderno-side question -- see caderno#16.
The desk is distributed from ~magbel. On any ship:
|install ~magbel %aviary
(To run it from a local checkout instead — for development, or to install from your own ship — see the development loop below.)
Then in caderno: create a notebook, choose kernel "aviary". Kernel
discovery needs the /x/sole/sessions scry (caderno's README notes
this requirement); the vendored lib/shoe.hoon provides it, so no extra
setup is needed on aviary's side.
desk/
sys.kelvin [%zuse 408]
desk.bill :~ %aviary ==
app/aviary.hoon shoe agent (thin transport shim over lib/aviary)
lib/aviary.hoon the pure engine: lexer, parser, registry, reducer,
bracket abstraction, magics, pretty-printer
sur/aviary.hoon term/bird/def/env types
tests/lib/aviary.hoon -test-thread-style regression tests
lib/shoe.hoon VENDORED from north master (%eval-command + the
/x/sole/sessions scry live here)
lib/sole.hoon, lib/default-agent.hoon, lib/dbug.hoon, lib/skeleton.hoon,
lib/test.hoon, sur/sole.hoon, mar/eval-command.hoon,
mar/bill.hoon, mar/sole/action.hoon, mar/sole/effect.hoon,
lib/language-server-complete.hoon, lib/language-server-parser.hoon
VENDORED, byte-for-byte, from north master /
base master (see SPEC-DESK.md §1-2 for exactly
which and why; the last five surfaced only when
actually installing on a live ship -- desk.bill
needs mar/bill.hoon to validate, Eyre needs
mar/sole/{action,effect}.hoon to JSON-serialize
sole-effect facts for any HTTP/channel client,
and lib/shoe.hoon's tab-completion needs the
two flat-named language-server-*.hoon files)
tests/
test-engine.sh headless engine tests via `urbit eval` (SPEC-
DESK.md §8); needs $URBIT_BIN or ~/bin/urbit
test-engine-cases.hoon the actual §8 test battery (one Hoon expression)
tests/test_hoon_registry.py Python <-> Hoon registry cross-test (SPEC-
DESK.md §7): fails hard on any drift
Run the Hoon engine tests with make test-hoon (or bash tests/test-engine.sh directly); $URBIT_BIN overrides the urbit
binary used (defaults to ~/bin/urbit, falling back to urbit on
PATH). Run everything, Python and Hoon, with make test-all.
|mount %aviary
:: rsync/copy desk/ into the mounted pier directory, e.g.:
rsync -a desk/ /path/to/pier/aviary/
|commit %aviary
Then either talk to it directly from dojo (|shoe %aviary-style
interactive session, once mounted as a running app) or drive it from
caderno as above.