test test test.

This plot is generated at build time by a simple script:

Experiment plot

Runnable WASM demo

Output will appear here.

Embedded JSON

Loading…

Rust Code Sample

// Simple Rust example to demonstrate syntax highlighting
fn main() {
    let nums = [1, 2, 3, 5, 8, 13];
    let sum: i32 = nums.iter().sum();
    println!("Sum is {}", sum);
}

Latex Test

automaton
Figure 1. Finite automaton

Typst Test

complex plane

Untyped Impure Lambda Reduction Cube

There are 3 axes:

  • Redex Selection

    • Outermost (leftmost-outermost)

    • Innermost (leftmost-innermost)

  • λ-Restriction

    • Unrestricted (reduction under lambda abstractions allowed)

    • Abstraction-restricted (reduction under lambda abstractions not allowed)

  • β-Restriction (What is considered a redex)

    • Unrestricted (arguments to an application don’t have to be a value)

    • Value-restricted (arguments to an application have to be a value)

Key:

  • λNO: Normal-Order reduction

  • λAO: Applicative-Order reduction

  • λCBN: Call-By-Name reduction (the same as Weak Normal-Order reduction)

  • λCBV: Call-By-Value reduction

  • λWAO: Weak Applicative-Order reduction

  • λWNO: Weak Normal-Order reduction (the same as Call-By-Name reduction)

cube
Figure 2. Cube

Please note - selection and λ-restriction (λ-restriction is also known as strong and weak) are common in literature while β-restriction is not. In fact, most of the time Call-By-Value reduction is considered the same as Weak Applicative-Order reduction. In pure lambda calculus, this is true! However, if we concern ourselves with impure lambda calculus, we must restrict what is considered a redex. Selection and λ-restriction are positional in nature, with one determining which redex to contract first and the other blocking some redexes from being contracted. Note that this isn’t detereming what is a redex, just which one is contracted first. β-Restriction is different, in that it also determines what is a redex to begin with. β-Restricted evaluation says that (λx.M) N is not a redex if N is not a value.

To show the reason why β-Restriction is its own axis, I’ll show you how it differentiates Weak Applicative-Order reduction from Call-By-Value reduction in impure lambda calculus (remember, they’re the same in pure lambda calculus). Lets say we have an impure lambda calculus where the natural numbers are values. Let’s say we have the following term: (λx.x) (2 7). In Weak Applicative-Order reduction, this’d fully reduce to (2 7). In Call-By-Value reduction (which is β-Restricted), this wouldn’t reduce at all - it’d stay as (λx.x) (2 7). In the pure lambda calculus, however, the "2" and "7" would themselves be lambda abstractions of some form. Because of this, both Weak Applicative-Order reduction and Call-By-Value reduction would reduce this to the same result (which would be "14", if "2" and "7" are Church numerals).

This is all to say that if we are only concerning ourselves with pure lambda calculus, the β-Restriction axis could be removed entirely!