▼The Verse Calculus, in Redex
On this page:
The Verse Calculus, in Redex
9.2
Racket
  top  contents  ← prev  up   

The Verse Calculus, in Redex🔗ℹ

dannypsnl

 (require verse-calculus-redex)
  package: verse-calculus-redex

verse-calculus-redex is a PLT Redex formalization of the core Verse Calculus, from the paper The Verse Calculus: a Core Calculus for Functional Logic Programming. This manual is in two parts. The core calculus presents the calculus itself — its grammar and reduction rules, typeset from the live Redex model. Learn the calculus by steps teaches the calculus by example: each chapter walks through one paper derivation step by step, with every figure generated from the model when the manual is built, so the figures cannot drift from the code.

    1 The core calculus

      1.1 Grammar

      1.2 Reduction rules

    2 Learn the calculus by steps

      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  ← prev  up