Skip to content

A λ-term you can hear

What might a computation sound like as it runs? Let's reduce a λ-term step by step and turn its reactions into a rhythm you can listen to. lambdaterms.kt parses the term and compiles it to an interaction net (a graph of agents that rewrites itself one connected pair, a reaction, at a time), and the Reducer in interactionnets.kt fires one reaction at a time, reporting each as a ReductionStep. LambdaSoundDocs records those steps as a time series. patCondense, which runs the mini-notation parser backwards, finds the shortest notation that plays the resulting step mask, and patRenderStereo plays it.

A pattern with a figure in it condenses to a shorter notation than one without, so the notation patCondense returns tells you something about the order the reactions fired in. That order is what changes when you change the scheduler.

One reduction, recorded

three two is Church exponentiation the other way round: the numeral three applied to the numeral two, which is 2³. Most of its reactions are not β-steps (applying a function to its argument) but the bookkeeping that keeps sharing correct: fans copying, and scope delimiters (the agents that mark where a shared function body begins and ends) moving and closing. The box below reduces it and plots the size of the net after each reaction.

:::static
// trace() compiles, reduces and records; it does not relax the layout, because nothing is
// watching. The answer it read back is checked against the plain normal-order evaluator below.
val t = LambdaSoundDocs.trace("church-exp-two-cubed", ActivationOrder.FIRST_FOUND)

:::fold the net's size, the choice the scheduler had, and what came out
showSignals(
    "agents standing" to t.nodeSeries,
    "pairs a rule covers" to t.choiceSeries,
    // Short, because a plotly title wider than the plot is clipped rather than wrapped.
    title = "three two: after each of its 86 reactions",
    xTitle = "reaction",
    channel = "series",
)

markdown(
    "readout",
    """
| | |
|---|---|
| term | `${t.source}` |
| compiled to | ${t.initialNodes} agents, ${t.fans} fans |
| reactions | ${t.steps} |
| of those, β | ${t.betas} |
| rules fired | ${t.ruleTally.entries.joinToString(", ") { "`${it.key}` x${it.value}" }} |
| read back as | `${t.printed}` |
| left standing | ${t.remainingNodes} agents, ${t.trailingReduciblePairs} pairs a rule covers |
""",
    width = 1080,
)
:::endfold

A two-trace plot over eighty-six reactions: an agent count that climbs from about nineteen to a peak of forty-six around reactions thirty-five and forty-five and then falls, in steps, to twenty-six, and a lower trace of covered pairs that rises to fifteen and comes back down to zero, above a table giving the term, nineteen agents and three fans compiled, eighty-six reactions of which eight are beta, the rule tally led by delim-delim, and the answer λa. λb. a applied eight times to b

The lower trace is how many reactions were available at each moment, which is how much choice the scheduler had. It stays small throughout: only a handful of pairs are ready to react at any time, and the scheduler's job is to pick among them.

The scheduler does not change how long it takes

Reducer takes an ActivationOrder, which chooses the next active pair to fire. The order can change, but the reaction count and the number of times each rule fires stay the same. The box below reduces every term in the λ front end's corpus under all four schedulers and fails if any term breaks either rule.

:::static
/*
Both of these throw rather than return false. Reaching the next line is the measurement:
stepCountIsScheduleInvariant names the term and the counts if any term breaks it, and
ruleMultisetIsScheduleInvariant is the stronger claim that the mixes match too.
*/
val sweep = LambdaSoundDocs.corpusSweep()
val counts = LambdaSoundDocs.stepCountIsScheduleInvariant(sweep)
val multisets = LambdaSoundDocs.ruleMultisetIsScheduleInvariant(sweep)
val spellings = LambdaSoundDocs.spellingsPerTerm(sweep)

:::fold the corpus, worst-spread first
val rows =
    sweep.entries
        .filter { counts.getValue(it.key) > 0 }
        .sortedWith(
            compareByDescending<Map.Entry<String, Map<ActivationOrder, LambdaSoundDocs.Trace>>> {
                    spellings.getValue(it.key)
                }
                .thenByDescending { counts.getValue(it.key) },
        )
        .joinToString("\n") { (name, traces) ->
            val first = traces.values.first()
            "| `$name` | ${counts.getValue(name)} | ${first.betas} | ${first.fans} | " +
                "${spellings.getValue(name)} | `${first.betaCondensation.notation}` |"
        }

markdown(
    "sweep",
    """
${sweep.size} terms x ${LambdaSoundDocs.ORDERS.size} schedulers = ${sweep.size * LambdaSoundDocs.ORDERS.size} reductions.
Reaction count is scheduler-invariant on **all ${counts.size}**; so is the rule multiset, on all $multisets.
Three corpus terms are already normal forms and are left out of the table.

| term | reactions | β | fans | distinct β spellings | the FIRST_FOUND spelling |
|---|---|---|---|---|---|
$rows
""",
    width = 1120,
)
:::endfold

A table of twenty-two corpus terms sorted by reaction count, from church-pred-three at 127 down to self-apply-identity at 10: every term but the last condenses to four distinct notations across the four schedulers, the last to three, and the FIRST_FOUND spellings are long mixtures of single strikes, rests and the odd replicate

This follows from a result of Lafont's: interaction nets are strongly confluent. Two reactions available at once involve disjoint pairs of agents, so firing one cannot destroy the other, and a strongly confluent system that terminates reaches its normal form in the same number of steps down every path.

What the scheduler does change

Because the order differs, the β-steps land in different places, and patCondense can return a different notation for each scheduler. The box below takes three two under all four schedulers and draws where its β-steps fall.

:::static
/*
The same term the two clips below play, under each of the four reproducible schedulers.
answerIsScheduleInvariant checks all four against the plain normal-order evaluator, so the
"one answer" column is a measurement and not a caption.
*/
val traces = LambdaSoundDocs.traceAllOrders(LambdaSoundDocs.BAR_TERM)
val answer = LambdaSoundDocs.answerIsScheduleInvariant(traces)
val betas = LambdaSoundDocs.betaIsScheduleInvariant(traces)

:::fold the four beta masks as lanes, then their spellings
showPatRollOf(
    *traces.map { (order, t) -> order.name to t.betaCondensation.pattern }.toTypedArray(),
    title = "three two: where the $betas beta-steps fall, under four schedulers",
    subtitle = "one slot per reaction, ${traces.values.first().steps} reactions, one cycle each",
    cycles = 1,
    channel = "masks",
)

val rows =
    traces.entries.joinToString("\n") { (order, t) ->
        "| `${order.name}` | ${t.steps} | ${t.betas} | `${t.betaCondensation.notation}` | " +
            "${t.betaCompression.f2} | ${t.betaCondensation.exact} |"
    }
markdown(
    "spellings",
    """
All four read back as `$answer`.

| scheduler | reactions | β | shortest notation | against a flat spelling | the search signed for it |
|---|---|---|---|---|---|
$rows
""",
    width = 1080,
)
:::endfold

Four coloured piano-roll lanes of one cycle each, all with eight strikes in eighty-six slots but in visibly different places: FIRST_FOUND spreads four through the first half and packs its last four together near the end, LEFTMOST_BY_ID and HIGHEST_PAIR_ENERGY break theirs into pairs, and RIGHTMOST_BY_ID puts four early and spreads its last four out singly. Below, all four read back as the same answer, and a table gives every scheduler the same eighty-six reactions and eight betas against four different condensed notations and compressions of 0.20, 0.28, 0.26 and 0.27, all four signed for by the search

FIRST_FOUND lands its last four β-steps together near the end of the bar and the notation says so: a long rest and then x!4. RIGHTMOST_BY_ID spreads its last four out, so its notation has no replicate at all, only single strikes and rests. Nothing in the condenser knows what a λ-term is; it is looking for the shortest string that plays what it was handed.

Compression is a ratio of characters, so the length of the atom affects it. Both bars above use x, as the CA chain does. Compare two notations only when they use the same atom.

Here is FIRST_FOUND's bar, three cycles at 0.4 cycles per second:

Now listen to RIGHTMOST_BY_ID. It reaches the same answer with eighty-six reactions and eight β-steps, but fires them in a different order:

The two clips have the same strikes, voice and tempo, so they match in length and loudness. They differ only in where the strikes fall.

The reduction as pitch

A rule emits an event when it fires. A closed term emits six kinds of event: beta, branch, prune and annihilate, and scope and unscope for a scope delimiter moving and closing. Map those to six degrees of a minor pentatonic and a reduction becomes a tune whose notes are its rule sequence.

val notes = LambdaSoundDocs.trace("erase-argument").melody

// -> one MIDI note per reaction, pitched by the kind that reaction emitted

K I (mul 2 3) is the corpus's erasing term: it computes six and throws it away. Nine of its 120 reactions are prune, taking the discarded multiplication apart agent by agent, because an interaction net cannot simply drop a wire; most of the rest are scope and unscope.

Where each piece is documented