►The Verse Calculus, in Redex
▼2 Learn the calculus by steps
9.2
Racket
  top  contents    up   

2 Learn the calculus by steps🔗ℹ

This part teaches the calculus by example. Each chapter collects a machine-checked trace of one paper derivation, walking through it step by step, with every figure — reduction diagrams and per-step typesetting — generated from the Redex model when the manual is built. In every diagram, each node shows the paper notation above its s-expression form, and gray ↪ stubs mark the other rules that could legally fire at that state. Each path starts from (one _) wrapping the program, exactly as run does (Fig 1: a program is evaluated under one).

    2.1 How the traces are verified

    2.2 Exploring reduction graphs interactively

    2.3 Tracing §1: two views of one tuple

      2.3.1 Step 1 — SUBST

      2.3.2 Step 2 — U-TUP

      2.3.3 Step 3 — HNF-SWAP

      2.3.4 Step 4 — EQN-ELIM

      2.3.5 Step 5 — SUBST

      2.3.6 Step 6 — EQN-ELIM

      2.3.7 Step 7 — EQN-ELIM

      2.3.8 Step 8 — ONE-VALUE

      2.3.9 Why a curated path?

    2.4 Tracing §2.2: residuation

      2.4.1 Step 1 — SUBST

      2.4.2 Step 2 — EQN-ELIM

      2.4.3 Step 3 — APP-ADD

      2.4.4 Step 4 — SUBST

      2.4.5 Step 5 — EQN-ELIM

      2.4.6 Step 6 — ONE-VALUE

    2.5 Tracing §2.1: first⟨2,5⟩

      2.5.1 Step 1 — APP-BETA

      2.5.2 Step 2 — SUBST

      2.5.3 Step 3 — EQN-ELIM

      2.5.4 Step 4 — U-TUP

      2.5.5 Step 5 — HNF-SWAP

      2.5.6 Step 6 — EQN-ELIM

      2.5.7 Step 7 — HNF-SWAP

      2.5.8 Step 8 — SUBST

      2.5.9 Step 9 — EQN-ELIM

      2.5.10 Step 10 — ONE-VALUE

    2.6 Tracing §2.5: if/then/else, both branches

      2.6.1 The true branch

        2.6.1.1 Step 1 — U-LIT

        2.6.1.2 Step 2 — ONE-VALUE

        2.6.1.3 Step 3 — ONE-CHOICE

      2.6.2 The false branch

        2.6.2.1 Step 1 — U-FAIL

        2.6.2.2 Step 2 — ONE-FAIL

        2.6.2.3 Step 3 — CHOOSE-R

        2.6.2.4 Step 4 — ONE-VALUE

    2.7 Tracing §2.6: tuple indexing as choice

      2.7.1 Step 1 — APP-TUP

      2.7.2 Step 2 — EXI-SWAP

      2.7.3 Step 3 — VAR-SWAP

      2.7.4 Step 4 — EQN-ELIM

      2.7.5 Step 5 — CHOOSE (first)

      2.7.6 Step 6 — CHOOSE (second)

      2.7.7 Steps 7–9 — EQN-ELIM ×3

      2.7.8 Step 10 — ALL-CHOICE

      2.7.9 Step 11 — ONE-VALUE

  top  contents    up