7.7

5.1 The Core Calculus

Part 1 of 3 in the Tutorial: From Models to Interpreters.

    5.1.1 Syntax

      5.1.1.1 Abstract Syntax

      5.1.1.2 The Parser

      5.1.1.3 The Printer

      5.1.1.4 Values

    5.1.2 Evaluation Semantics

      5.1.2.1 Applications

      5.1.2.2 Sequences

      5.1.2.3 Simple Reduction

      5.1.2.4 Full Reduction

      5.1.2.5 The Full Stepper

    5.1.3 Pattern Matching Semantics

      5.1.3.1 The Cross Function

    5.1.4 Pragmatics

    5.1.5 Putting It All Together

    5.1.6 Examples

      5.1.6.1 Peano Numbers

      5.1.6.2 Peano Arithmetic & Recursion

      5.1.6.3 Boolean Logic

      5.1.6.4 Lists

    5.1.7 Closing Remarks

 #lang algebraic/model/core package: algebraic

the core model has three components:

Syntax

t

 

 

t t

 

    application

 

|

 

t;t

 

    sequence

 

|

 

φp.t

 

    function clause

 

|

 

μp.t

 

    macro clause

 

|

 

x

 

    variable

 

|

 

δ

 

    constructor

 

|

 

 

    unit

p

 

 

t t

 

    application

 

|

 

t;t

 

    sequence

 

|

 

_

 

    wildcard

 

|

 

x

 

    variable

 

|

 

δ

 

    constructor

 

|

 

 

    unit

v

 

 

φp.t

 

    function

 

|

 

μp.t

 

    macro

 

|

 

δ

 

    constructor

 

|

 

δ (v;·)

 

    instance

 

|

 

 

    unit

Evaluation Semantics

t1  t1'

t1 t2  t1' t2

 

APP1

v1≁μp.t

   

t2  t2'

v1 t2  v1 t2'

 

APP2

t1  t1'

t1;t2  t1';t2

 

SEQ1

t2  t2'

v1;t2  v1;t2'

 

SEQ2

p11×v2

   

σ(t12)=t12'

p11.t12) v2  t12'

 

APPF

p11×t2

   

σ(t12)=t12'

p11.t12) t2  t12'

 

APPM

p11.t12) v2  t12'

p11.t12;v13) v2  t12'

 

FUN1

p11×v2 undefined

p11.t12;v13) v2  v13 v2

 

FUN2

p11.t12) t2  t12'

p11.t12;v13) t2  t12'

 

MAC1

p11×t2 undefined

p11.t12;v13) t2  v13 v2

 

MAC2

Pattern Matching Semantics

p11×t21 = σ1

   

p12×t22 = σ2

(p11 p12)×(t21 t22) = σ1 ∪ σ2

p11×t21 = σ1

   

p12×t22 = σ2

(p11;p12)×(t21;t22) = σ1 ∪ σ2

x1×t2 = {x1t2}

δ1 = δ2

δ1×δ2 = {}

t1 = {}

◊×◊ = {}

Example Programs

fix

=

φf.(φx.fy.(x x) y)) (φx.fy.(x x) y))

add

=

φ(n Zero).n;φ(n (Succ m)).Succ(add (n m))

mul

=

φ(n Zero).Zero;φ(n (Succ m)).add(n (mul (n m)))

not

=

φFalse.True;φ_.False

and

=

μ(a b).(φFalse.False;φ_.b) a

or

=

μ(a b).(φFalse.bx.x) a

xor

=

μ(a b).(φFalse.bx.and ((not b) x)) a

list

=

μ(x ◊).Cons(x;Nil);μ(x xs).Cons(x;list xs)

reverse

=

φxs.rev(xs Nil)

rev

=

φ(Nil a).a;φ(Cons(x;xs) a).rev(xs Cons(x;a))

5.1.1 Syntax

The core defines three syntactic categories: terms, values, and patterns.

A term (t) is a concrete expression in the calculus.

A value (v) is a term in normal form with respect to the evaluation semantics.

When a term eventually reduces to a particular value, we say the term evaluates to that value. A term may never reduce to a value if the computation diverges or gets stuck. Some divergent terms are useful as infinite loops. Any stuck term is an error.

A pattern (p) is a syntactic form that produces a set of variable bindings (σ) when matched with a compatible term.

An application (t t) is a pair of juxtaposed sub-terms. Nested applications are always parenthesized.

  (A )

A sequence (t;t) is a pair of sub-terms separated by a semicolon in the model and prefixed by a dollar sign ($) in code. Sequences combine multiple terms into a single unit. They are used for holding the non-tag elements of a tagged list.

  (A ($  ))

A function clausep.t) or macro clausep.t) is a λ-abstraction with the formal parameter generalized to a pattern.

  (φ x x)
  (μ a a)

A uniform sequence (t;·) is a right-hand nesting of sequences in which every left-hand side holds the same kind of term and every right-hand side, except perhaps the last, is the same kind of uniform sequence. Uniform sequences combine multiple abstractions into a single unit.

A functionp.t;·) is a function clause or a uniform sequence of them, and a macro (μp.t;·) is one or more macro clauses in sequence.

  ($ (φ x x) ($ (φ y y) (φ z z)))
  ($ (μ a a) ($ (μ b b) (μ c c)))

A variable (x) is a name that may be bound to a term in the body of a function clause or macro clause. We say a variable not bound by an abstraction is free. All free variables are stuck.

A constructor (δ) is a name that identifies a data type. Constructors evaluate to themselves.

For convenience, constructor names begin with an uppercase letter and variable names begin with a lowercase letter.

An instance (δ (v;·)) is a constructor applied to a value or sequence of values.

  (A )
  (B ($  ))

Finally, the unit (◊) value denotes the presence of a value, as a convenient notation for when the actual value is irrelevant.

5.1.1.1 Abstract Syntax

According to the formal syntax, we need seven kinds of terms and six kinds of patterns.

  (data Term (TApp TSeq TFun TMac TVar TCon TUni)
        Patt (PApp PSeq PWil PVar PCon PUni))

Abstract syntax drives the interpreter, but it makes a poor surface syntax. We might have to cross-check the code and the model several times, so it would be convenient to have a surface syntax that resembles the formal syntax.

5.1.1.2 The Parser

The parser’s job is to map s-expressions onto the members of Term. Some terms have a pattern, and patterns are parsed by different rules than terms. Although constructor arities are not encoded in the data declaration, we can anticipate the following:

With these points in mind, the parser will look like this:

  (define (parse t)
    (define term
      (function
        [(   t1 t2) (TApp (term t1) (term t2))]
        [('$ t1 t2) (TSeq (term t1) (term t2))]
        [('φ p1 t2) ... (TFun ...) ...]
        [('μ p1 t2) ... (TMac ...) ...]
        [x #:if (con-name? x) (TCon x)]
        [x #:if (var-name? x) (TVar x)]
        [' TUni]))
    (define patt
      (function
        [(   p1 p2) (PApp (patt p1) (patt p2))]
        [('$ p1 p2) (PSeq (patt p1) (patt p2))]
        [x #:if (con-name? x) (PCon x)]
        [x #:if (var-name? x) (PVar x)]
        ['_ PWil]
        [' PUni]))
    (term t))

The parse function is defined as a pair of s-expression parser combinators: term and patt. The term combinator translates terms in the formal syntax onto Term, while patt maps patterns in the formal syntax onto Patt. Parsing always starts and ends with a single term.

We need a way to tell constructor names from variable names. Inspecting characters directly is noisy; This is an s-expression parser, so we’ll put the logic into helper predicates: con-name? will check if the first character is uppercase and var-name? will check if it’s lowercase.

  (define (con-name? x)
    (and (symbol? x) (char-upper-case? (first-char x))))
   
  (define (var-name? x)
    (and (symbol? x) (char-lower-case? (first-char x))))
   
  (define (first-char s) (string-ref (symbol->string s) 0))

But what about the abstraction parsers? Pure structural recursion is an option, but we can save a lot of trouble later if we do a little extra work in the parser. We’re talking, of course, about unintended variable capture.

The following is a typical example of unintended variable capture:

  ((φ x (φ y (x y))) y)

In the next step of this function application, the outer function will reduce to the inner function with all of the xs replaced with ys. If we perform the substitution naively, we get a function clause wherein the free outer y is indistinguishable from the bound inner y:

  (φ y (y y))

Unintended variable capture is a well-studied problem with multiple solutions. Our goal is to produce correct code that is easy to read, so we’ll take a straight-forward approach of uniquely renaming all non-free variable names as they are parsed. This is equivalent to rewriting the original s-expression so every bound variable gets a unique index. For example, the original term could be rewritten as:

  ((φ x1 (φ y2 (x1 y2))) y)

Reducing this term does not lead to the unintended capture of y2.

  (φ y2 (y y2))

Later, we’ll implement a function named α-rename to automate this variable-renaming process. For now, we’ll just use it to finish the parse function.

  (define (parse t)
    (define term
      (function
        [(   t1 t2) (TApp (term t1) (term t2))]
        [('$ t1 t2) (TSeq (term t1) (term t2))]
        [('φ p1 t2) (values-> TFun (α-rename (patt p1) (term t2)))]
        [('μ p1 t2) (values-> TMac (α-rename (patt p1) (term t2)))]
        [x #:if (con-name? x) (TCon x)]
        [x #:if (var-name? x) (TVar x)]
        [' TUni]))
    (define patt
      (function
        [(   p1 p2) (PApp (patt p1) (patt p2))]
        [('$ p1 p2) (PSeq (patt p1) (patt p2))]
        [x #:if (con-name? x) (PCon x)]
        [x #:if (var-name? x) (PVar x)]
        ['_ PWil]
        [' PUni]))
    (term t))
   
  (define-syntax values-> (μ* (f xs-expr) (call-with-values (λ () xs-expr) f)))

The α-rename function takes a Patt and a Term. It returns two values: a copy of the Patt with all of its variables renamed, and a copy of the Term with its variables renamed as they were in the Patt.

The values-> macro is a simple syntactic patch for call-with-values that rearranges the arguments for a more compact applicative style.

5.1.1.3 The Printer

The printer’s job is to translate the members of Term back into s-expressions. The printer has the same structure as the parser, but the roles of pattern and body are swapped.

The show function is also defined as a pair of term / patt combinators. This time, each function pattern deconstructs a member of Term or Patt and produces a term or pattern in the formal syntax as an s-expression. A helper named α-restore is introduced pre-emptively to undo whatever α-rename does to variable names.

5.1.1.4 Values

Operationally, a value is a term that evaluates to itself trivially. Values are the subset of terms that constitute a valid computational result. To recognize them, we’ll need a series of predicates on the members of Term.

Our goal is to produce a value? predicate that checks whether a Term is:

To do all this, we need to recognize three kinds of uniform sequence: functions, macros, and instance data.

  (define-syntax define-uniform-sequence-pred
    (μ* (name? kind?)
      (define name?
        (function
          [(TSeq t1 t2) #:if (kind? t1) (name? t2)]
          [t (kind? t)]))))
   
  (define-uniform-sequence-pred fun? TFun?)
  (define-uniform-sequence-pred mac? TMac?)
  (define-uniform-sequence-pred dat? value?)

A define-uniform-sequence-pred form takes two arguments: a name to bind and a predicate name. It binds the name to a new predicate for uniform sequences of terms satisfying the named predicate.

The fun?, mac?, and dat? predicates recognize a uniform sequence of function clauses, macro clauses, and values, respectively.

  (define ins? (function [(TApp (TCon _) t) (dat? t)] [_ #f]))

The ins? predicate recognizes an instance as a constructor applied to instance data. Although instance data is not strictly uniform, thinking of it as a “uniform” sequence of values is convenient because the predicates all have the same shape.

  (require racket/contract/base)
   
  (define value? (or/c fun? mac? TCon? ins? TUni?))

The value? predicate combines all three uniform sequence predicates with the TCon? and TUni? predicates generated by our data declaration to cover all five cases.

5.1.2 Evaluation Semantics

Every interpreter in the tutorial series provides a “top level” evaluator macro named algebraic which:

  1. parses an unquoted s-expression as a Term,

  2. attempts to evaluate the Term to a value?, and

  3. shows the result.

The interpret function will drive the computation of t in a tight loop that calls another function named step until it returns a value?.

The step function will take a Term for the current step of a computation and return the next step or #f if stuck.

If a term gets stuck, we’ll want to trace the steps of the computation to figure out what went wrong. We could just toggle the commented middle line in a pinch, but the conditional looping behavior of interpret is easy to capture with a macro.

The colon-delimited syntax class name (:id) labels some macro arguments as identifiers. These extra bits of notation give better error messages when something goes wrong.

A define-interpreter form looks like the define shorthand for a unary function. Its argument receives the current step of the computation and its body calculates the next step.

With define-interpreter, we can cleanly define the interpret function alongside a more verbose trace variant.

We still need a step function. Its job is to implement the semantics of our language. The core model consists of ten inference rules governing the evaluation of terms to values. Each rule corresponds to a clause of the step function. We’ll put each clause into its own function and have step try them in order.

The rule functions have a regular shape:

  (define step-name (function [pattern result] [_ #f]))

With a macro that abstracts away everything but the step-names, patterns, and results, our step definition will look like this:

  (define-stepper step
    (rule1 rule2 ... ruleN)
    [rule1 pattern1 result1]
    [rule2 pattern2 result2]
    ...
    [ruleN patternN resultN])

A define-stepper form with n rules defines n+1 names: a function for each rule and one more that tries them in the order specified.

  (define-syntax define-stepper
    (μ* (stepper-name:id
         (order:id ...+)
         [step-name:id pattern result] ...+)
      (begin
        (define (stepper-name t) (or (order t) ...))
        (define step-name (function [pattern result] [_ #f]))
        ...)))

The define-stepper macro expects a list of rule names in addition to definitions so we can change the order of application without having to move the definitions around.

5.1.2.1 Applications

t1  t1'

t1 t2  t1' t2

 

APP1

v1≁μp.t

   

t2  t2'

v1 t2  v1 t2'

 

APP2

Applications evaluate quasi-eagerly, starting on the left. If the left side is a macro, the macro will operate on the un-evaluated right side. Otherwise, evaluation proceeds to the right.

  (define-stepper step
    ...
    [app1 (TApp t1 t2) (let ([t1* (step t1)]) (and t1* (TApp t1* t2 )))]
    [app2 (TApp v1 t2) (let ([t2* (step t2)]) (and t2* (TApp v1  t2*)))]
    ...)

This defines two functions: app1 and app2.

The app1 function takes a TApp with two sub-terms and tries to step the first. If successful, it returns a copy of the TApp with the new first sub-term. Otherwise, it returns #f.

The app2 function does essentially the same thing with the second sub-term of a TApp. If we always try app1 first, we can assume the first sub-term of a TApp is fully evaluated in app2.

Most of the rules have this (let ([t* ...]) (and t* ...)) form, so we’ll put it in a macro.

  (define-syntax sub-step
    (μ* (t*-expr t*:id result)
      (let ([t* t*-expr]) (and t* result))))

The sub-step form expresses structural recursion a little more compactly:

  (define-stepper step
    ...
    [app1 (TApp t1 t2) (sub-step (step t1) t1* (TApp t1* t2 ))]
    [app2 (TApp v1 t2) (sub-step (step t2) t2* (TApp v1  t2*))]
    ...)

5.1.2.2 Sequences

t1  t1'

t1;t2  t1';t2

 

SEQ1

t2  t2'

v1;t2  v1;t2'

 

SEQ2

Sequences always evaluate eagerly from left to right.

  (define-stepper step
    ...
    [seq1 (TSeq t1 t2) (sub-step (step t1) t1* (TSeq t1* t2 ))]
    [seq2 (TSeq v1 t2) (sub-step (step t2) t2* (TSeq v1  t2*))]
    ...)

5.1.2.3 Simple Reduction

p11×v2

   

σ(t12)=t12'

p11.t12) v2  t12'

 

APPF

p11×t2

   

σ(t12)=t12'

p11.t12) t2  t12'

 

APPM

Function clauses attempt to match a single argument value to a pattern. If the match succeeds, any variables bound by the pattern are substituted into the body of the function. If the match fails, the term is stuck.

Macro clauses work similarly. The only semantic difference between function clauses and macro clauses is that macro clauses do not evaluate their argument before attempting the match.

  (define-stepper step
    ...
    [appF (TApp (TFun p11 t12) v2) (sub-step (× p11 v2) σ (subst σ t12))]
    [appM (TApp (TMac p11 t12) t2) (sub-step (× p11 t2) σ (subst σ t12))]
    ...)

The × (“cross”) function defines the semantics of pattern matching. It takes a Patt and a Term and returns a hash named σ as described in the next section.

The subst function implements variable substitution. Here, it takes two arguments: a hash σ and a term t12. The hash maps variable names to Terms, and subst applies those mappings to t12 recursively.

  (require racket/set)
   
  (define (subst σ t [mask (seteq)])
    ((function
       [(TApp t1 t2) (TApp (subst σ t1 mask) (subst σ t2 mask))]
       [(TSeq t1 t2) (TSeq (subst σ t1 mask) (subst σ t2 mask))]
       [(TFun p1 t2) (TFun p1 (subst σ t2 (set-union mask (vars p1))))]
       [(TMac p1 t2) (TMac p1 (subst σ t2 (set-union mask (vars p1))))]
       [(TVar x1) (if (set-member? mask x1) t (hash-ref σ x1))]
       [(TCon _) t]
       [TUni t])
     t))

The subst function passes around an optional set named mask to remember which variables are already bound in the active substitution context. This is how we prevent unintended variable capture. Thanks to α-rename, variable names can be compared directly with eq?.

  (define vars
    (function
      [(PApp p1 p2) (set-union (vars p1) (vars p2))]
      [(PSeq p1 p2) (set-union (vars p1) (vars p2))]
      [(PVar x1) (seteq x1)]
      [(PCon _) (seteq)]
      [PWil (seteq)]
      [PUni (seteq)]))

The vars function takes a Patt and returns a set containing all of the variable names it binds.

It’s worth noting algebraic abstractions do not offer explicit syntax for default argument values. We could have implemented subst as a two-clause function*:

  (define subst
    (function*
      [(σ t) (subst σ t (seteq))]
      [(σ t mask)
       ((function ...) t)]))

Alternatively, we could have repeated the first and final arguments in every clause but the first:

  (define subst
    (function*
      [(σ t) (subst σ t (seteq))]
      [(σ (TApp t1 t2) mask) ...]
      [(σ (TSeq t1 t2) mask) ...]
      ...))

5.1.2.4 Full Reduction

p11.t12) v2  t12'

p11.t12;v13) v2  t12'

 

FUN1

p11×v2 undefined

p11.t12;v13) v2  v13 v2

 

FUN2

p11.t12) t2  t12'

p11.t12;v13) t2  t12'

 

MAC1

p11×t2 undefined

p11.t12;v13) t2  v13 v2

 

MAC2

Multi-clause functions and macros attempt to match their inputs to each clause in the sequence, taking the body of the first succesful match as their result. If every match fails, the term is stuck.

If we transcribe FUN1, FUN2, MAC1, and MAC2 directly from the operational semantics, our step function would look like this:

  (define-stepper step
    ...
    [fun1 (TApp (TSeq (TFun x t) v12) v2) (step (TApp (TFun x t) v2))]
    [mac1 (TApp (TSeq (TFun x t) v12) v2) (step (TApp (TFun x t) v2))]
    [fun2 (TApp (TSeq (TFun _ _) v12) v2) (TApp v12 v2)]
    [mac2 (TApp (TSeq (TFun _ _) v12) v2) (TApp v12 v2)]
    ...)

but these four rules can easily be merged into two:

  (define-stepper step
    ...
    [redF (TApp (TSeq (TFun x t) v12) v2) (or (step (TApp (TFun x t) v2)) (TApp v12 v2))]
    [redM (TApp (TSeq (TMac x t) v12) t2) (or (step (TApp (TMac x t) t2)) (TApp v12 t2))]
    ...)

and the structural similarity of these rules is compelling, given their length. We can keep our rule set compact by capturing the (or (step (TApp ...)) (TApp ...)) form in another macro.

  (define-syntax alt-step
    (μ* ((abs val) (alt alt-val))
      (or (step (TApp abs val)) (TApp alt alt-val))))

The alt-step form more compactly expresses this kind of choice.

  (define-stepper step
    ...
    [redF (TApp (TSeq (TFun x t) v12) v2) (alt-step ((TFun x t) v2) (v12 v2))]
    [redM (TApp (TSeq (TMac x t) v12) v2) (alt-step ((TMac x t) v2) (v12 v2))]
    ...)

5.1.2.5 The Full Stepper

When assembled, the rules define a complete step function.

  (define-stepper step
    (seq1 seq2 app1 appM redM app2 appF redF)
    [app1 (TApp t1 t2) (sub-step (step t1) t1* (TApp t1* t2 ))]
    [app2 (TApp v1 t2) (sub-step (step t2) t2* (TApp v1  t2*))]
    [seq1 (TSeq t1 t2) (sub-step (step t1) t1* (TSeq t1* t2 ))]
    [seq2 (TSeq v1 t2) (sub-step (step t2) t2* (TSeq v1  t2*))]
    [appF (TApp (TFun p11 t12) v2) (sub-step (× p11 v2) σ (subst σ t12))]
    [appM (TApp (TMac p11 t12) t2) (sub-step (× p11 t2) σ (subst σ t12))]
    [redF (TApp (TSeq (TFun x t) v12) v2) (alt-step ((TFun x t) v2) (v12 v2))]
    [redM (TApp (TSeq (TMac x t) v12) v2) (alt-step ((TMac x t) v2) (v12 v2))])

The rules appM and appF differ by a single product constructor. Their different behaviors are a consequence of the intervening rule app2.

5.1.3 Pattern Matching Semantics

Pattern matching (p×t=σ) is a binary operation on patterns and terms which produces a set of variable bindings when a pattern and term are compatible in one of the following six ways.

p11×t21 = σ1

   

p12×t22 = σ2

(p11 p12)×(t21 t22) = σ1 ∪ σ2

p11×t21 = σ1

   

p12×t22 = σ2

(p11;p12)×(t21;t22) = σ1 ∪ σ2

x1×t2 = {x1t2}

δ1 = δ2

δ1×δ2 = {}

t1 = {}

◊×◊ = {}

An application pattern (p p) matches an application if the sub-patterns and sub-terms all match by position, passing along any variable bindings.

A sequence pattern (p;p) behaves similarly.

A variable (x) matches any term and binds itself to the term.

A constructor pattern (δ) matches a constructor with the same name and binds no variables.

The wildcard (_) matches any term and binds no variables.

The unit pattern (◊) matches only the unit value.

Any other combination is undefined.

5.1.3.1 The Cross Function

The × function implements these six equations directly.

  (require racket/hash)
   
  (define ×
    (function*
      [((PApp p11 p12) (TApp t21 t22))
       (let ([σ1 (× p11 t21)]
             [σ2 (× p12 t22)])
         (and σ1 σ2 (hash-union σ1 σ2)))]
      [((PSeq p11 p12) (TSeq t21 t22))
       (let ([σ1 (× p11 t21)]
             [σ2 (× p12 t22)])
         (and σ1 σ2 (hash-union σ1 σ2)))]
      [((PCon δ) (TCon δ)) (make-immutable-hasheq)]
      [((PVar x1) t2) (make-immutable-hasheq `([,x1 . ,t2]))]
      [(PWil _) (make-immutable-hasheq)]
      [(PUni TUni) (make-immutable-hasheq)]
      [(_ _) #f]))

In the PCon / TCon clause, algebraic implicitly guarantees the pattern and term refer to the same constructor. When a function variable name appears more than once in a single function pattern, all of the values it binds must be equal?.

5.1.4 Pragmatics

It’s time to pay the piper.

  (define (α-rename p t)
    (define (term x y)
      (function
        [(TApp t1 t2) (TApp ((term x y) t1) ((term x y) t2))]
        [(TSeq t1 t2) (TSeq ((term x y) t1) ((term x y) t2))]
        [(TFun p1 t2) (TFun p1 ((term x y) t2))]
        [(TMac p1 t2) (TMac p1 ((term x y) t2))]
        [(TVar x1) (TVar (if (equal? x1 x) y x1))]
        [(TCon δ1) (TCon δ1)]
        [TUni TUni]))
    (define (patt x y)
      (function
        [(PApp p1 p2) (PApp ((patt x y) p1) ((patt x y) p2))]
        [(PSeq p1 p2) (PSeq ((patt x y) p1) ((patt x y) p2))]
        [(PVar x1) (PVar (if (equal? x1 x) y x1))]
        [(PCon δ1) (PCon δ1)]
        [PWil PWil]
        [PUni PUni]))
    (define p-vars (set->list (vars p)))
    (let loop ([xs p-vars]
               [ys (map genvar p-vars)]
               [p* p]
               [t* t])
      (if (null? xs)
          (values p* t*)
          (let ([p** ((patt (car xs) (car ys)) p*)]
                [t** ((term (car xs) (car ys)) t*)])
            (loop (cdr xs) (cdr ys) p** t**)))))
   
  (define genvar (φ x (string->uninterned-symbol (symbol->string x))))

The α-rename function builds on the term / patt combinator technique. It takes a Patt and a Term and returns copies with every variable bound by the Patt consistently renamed in both.

Most of the code is just plumbing for structural recursion, but the TVar and PVar cases are more interesting. If the name of a variable is equal? to x, we replace it with y.

The body loop does three things:

  1. Extracts the variables of a Patt,

  2. Generates uninterned symbols with the same names as the variables extracted, and

  3. Recursively substitutes the new names for the originals in both arguments.

The genvar function takes an interned symbol and generates an uninterned symbol with the same name. If we replace genvar with gensym, the bound variables will be tagged with unique numbers when parsed:

> (show (trace (parse/gensym '((φ x (φ y (x y))) y))))

((φ x32278 (φ y32277 (x32278 y32277))) y)

'(φ y32277 (y y32277))

There’s a wrinkle. We can’t tell the difference between two uninterned symbols with the same name by simply looking at them, but Racket can. If the show function prevents uninterned symbols from leaking to the surface, we can compare surface terms with equal? in unit tests.

The α-restore function will reconstruct the interned symbol for printing.

  (define (α-restore x)
    (string->symbol (symbol->string x)))

5.1.5 Putting It All Together

We now have a complete algebraic form for evaluating core terms.

This is good enough for unit testing, but it’s still a little clunky in interactive sessions. We won’t need to embed every term in an algebraic form if we turn the module into a #lang.

The algebraic package installs an algebraic/model collection that implements #langs for all of the tutorial interpreters. If you want to work with uninstalled modules, see the module form or #lang s-exp in the Module Languages section of The Racket Guide.

To do that, we need to write a little boilerplate. With everything in place, we should be able to enter a .rkt file with the first line set to #lang algebraic/model/core (or wherever your module is installed) and interact with the interpreter directly.

The default #%module-begin form wraps non-interactive top-level expressions, “to print non-#<void> results using current-print.” We wrap each top-level expression with an algebraic form.

The default #%top-interaction form wraps interactive top-level expressions as a hook into the default read-eval-print-loop. We also wrap top-level expressions with an algebraic form.

To replace the default top-level forms with our own, we’ll rename them on export. We also need to export the default #%app and #%datum forms because Racket will complain if we don’t.

  (provide (all-defined-out)
           (for-syntax (all-defined-out))
           #%app #%datum
           (rename-out
            [core-module-begin #%module-begin]
            [core-top-interaction #%top-interaction]))

Exporting the top-level forms this way makes our module work as a module language.

When a .rkt file begins with #lang algebraic/model/core, Racket uses a sub-module named reader to load our customizations:

  (module reader syntax/module-reader
    algebraic/model/core)

This file configures Racket to use algebraic/model/core as a module language with the default s-expression reader whenever it encounters a .rkt file that begins with #lang algebraic/model/core.

5.1.6 Examples

Examples are presented in two or three formats:

5.1.6.1 Peano Numbers

Peano numbers are an easy way to represent the natural numbers (0, 1, 2, ...) with algebraic data.

First, we designate a 0 element and define a successor function for it. A simple two-product sum will suffice.

> (data Peano (Zero Succ))

We can now define Peano numbers inductively:

Every natural number has a unique Peano encoding. If n is a natural number, its Peano encoding is a series of n Succs terminated by a Zero. The number 3, for example, is encoded as (Succ (Succ (Succ Zero))).

By definition, Zero is not the successor of any other Peano number, and Succ is an injective function from one Peano number to another. Whereas every Peano number is a member of the Peano sum, the converse is not true in general. Proving that an instance of Peano really is a Peano number takes some work:

> (define peano? (function [Zero #t] [(Succ n) (peano? n)] [_ #f]))
> (peano? (Succ Zero))

#t

> (peano? (Zero Succ))

#f

Now that we know what Peano number are, how do we use them?

5.1.6.2 Peano Arithmetic & Recursion

Addition (+) and multiplication (×) on Peano numbers are defined inductively:

n + 0

=

n

n + Succ m

=

Succ(n + m)

n × 0

=

0

n × Succ m

=

n + n × m

The core calculus can express these relationships directly:

add

=

φ(n Zero).n;φ(n (Succ m)).Succ(add (n m))

mul

=

φ(n Zero).Zero;φ(n (Succ m)).add(n (mul (n m)))

and so can algebraic:

> (define add
    (function*
      [(n Zero) n]
      [(n (Succ m)) (Succ (add n m))]))
> (add (Succ Zero) (Succ (Succ Zero)))

(Succ (Succ (Succ Zero)))

> (define mul
    (function*
      [(n Zero) Zero]
      [(n (Succ m)) (add n (mul n m))]))
> (mul (Succ (Succ Zero)) (Succ (Succ (Succ Zero))))

(Succ (Succ (Succ (Succ (Succ (Succ Zero))))))

Both functions have two clauses: a base case and an inductive step. The inductive step is a recursive call. If we had a letrec form, we could express the recursion directly:

  (letrec
      [add ($ (φ (a Zero) a)
              (φ (a (Succ b)) (Succ (add (a b)))))]
    (add ((Succ Zero) (Succ (Succ Zero)))))

But our interpreter just isn’t there yet. With a simple rewrite, we can express letrec as let plus a fixed-point combinator:

(letrec [id val] body)

(let [id (fix (φ id val))] body)

With a second rewrite, we can express let as a function application:

(let [id val] body)

((φ id body) val)

And if we fold this rewrite into the first one, the resulting form contains only functions and applications:

(letrec [id val] body)

(let [id (fix (φ id val))] body)

 

((φ id body) (fix (φ id val)))

The fix function gives us a way to encode functions that might call themselves.

fix = φf.(φx.fy.(x x) y)) (φx.fy.(x x) y))

With the following encoding of fix, our interpreter will be able to handle the functional encodings of let and letrec:

  (φ f
    ((φ x (φ f (φ y ((x x) y))))
     (φ x (φ f (φ y ((x x) y))))))

We’ll start with a program in the hypothetical syntax:

  (let [fix (φ f
              ((φ x (φ f (φ y ((x x) y))))
               (φ x (φ f (φ y ((x x) y))))))]
     (letrec [add ($ (φ (a Zero) a)
                     (φ (a (Succ b)) (Succ (add (a b)))))]
       (add ((Succ Zero) (Succ (Succ Zero))))))

and turn it into a runnable program with two rewrites. First, eliminate the outer let:

  ((φ fix
     (letrec [add ($ (φ (a Zero) a)
                     (φ (a (Succ b)) (Succ (add (a b)))))]
       (add ((Succ Zero) (Succ (Succ Zero))))))
   (φ f
     ((φ x (φ f (φ y ((x x) y))))
      (φ x (φ f (φ y ((x x) y)))))))

Second, eliminate the inner letrec:

  ((φ fix
     ((φ add
        (add ((Succ Zero) (Succ (Succ Zero)))))
      (fix (φ add ($ (φ (a Zero) a)
                     (φ (a (Succ b)) (Succ (add (a b)))))))))
   (φ f
     ((φ x (f (φ y ((x x) y))))
      (φ x (f (φ y ((x x) y)))))))

This program runs. It calculates 1 + 2 = 3 with Peano numbers. To run it, put the code in a .rkt file that begins with #lang "algebraic/model/core" and point Racket at the file.

> ((φ fix
     ((φ add
        (add ((Succ Zero) (Succ (Succ Zero)))))
      (fix (φ add ($ (φ (a Zero) a)
                     (φ (a (Succ b)) (Succ (add (a b)))))))))
   (φ f
     ((φ x (f (φ y ((x x) y))))
      (φ x (f (φ y ((x x) y)))))))

'(Succ (Succ (Succ Zero)))

We can even turn it into a unit test inside the algebraic/model/core module:

By similar treatment, we can transform the hypothetical program:

  (let [fix (φ f
              ((φ x (φ f (φ y ((x x) y))))
               (φ x (φ f (φ y ((x x) y))))))]
     (letrec [add ($ (φ (a Zero) a)
                     (φ (a (Succ b)) (Succ (add (a b)))))]
       (letrec [mul ($ (φ (a Zero) Zero)
                       (φ (a (Succ b)) (add (a (mul (a b))))))]
         (mul ((Succ (Succ Zero)) (Succ (Succ (Succ Zero))))))))

into a runnable program that computes 2 × 3 = 6 with Peano numbers in three rewrites:

> ((φ fix
     ((φ add
        ((φ mul
           (mul ((Succ (Succ Zero)) (Succ (Succ (Succ Zero))))))
         (fix (φ mul ($ (φ (a Zero) Zero)
                        (φ (a (Succ b)) (add (a (mul (a b))))))))))
      (fix (φ add ($ (φ (a Zero) a)
                     (φ (a (Succ b)) (Succ (add (a b)))))))))
   (φ f
     ((φ x (f (φ y ((x x) y))))
      (φ x (f (φ y ((x x) y)))))))

'(Succ (Succ (Succ (Succ (Succ (Succ Zero))))))

5.1.6.3 Boolean Logic

The Booleans are a popular example of an enumerated type. Assuming two constructors False and True that take no arguments, logical negation is a short function.

not

=

φFalse.True;φ_.False

Logical conjunction and disjunction, however, should exhibit “short circuiting” behavior so only the arguments needed to determine the result are evaluated. Encoding that behavior in only functions is tedious, but macros make short work of it. We’ll also throw in a smart xor macro for kicks.

and

=

μ(a b).(φFalse.False;φ_.b) a

or

=

μ(a b).(φFalse.bx.x) a

xor

=

μ(a b).(φFalse.bx.and ((not b) x)) a

For all of these operations, any non-False value is equivalent to True, and the original value is preserved in the result wherever possible.

The and macro takes two arguments, a and b. The outer macro gets a and b un-evaluated and forces the evaluation of a with an inner anonymous function which maps non-False values to b.

The or macro uses the same approach, this time evaluating b only if a evaluates to False.

The xor macro goes through a little extra trouble to return the original value when its result is not False. If a and b both evaluate to False or non-False, the result is False. Otherwise, the result is the non-False value.

not

=

($ (φ False True) (φ _ False))

and

=

(μ (a b) (($ (φ False False) (φ _ b)) a))

or

=

(μ (a b) (($ (φ False b) (φ x x)) a))

xor

=

(μ (a b) (($ (φ False b) (φ x (and ((not b) x)))) a))

To combine these macros with the technique covered in the previous section, we start with the hypothetical program:

  (let [not ($ (φ False True) (φ _ False))]
    (let [and (μ (a b) (($ (φ False False) (φ _ b)) a))]
      (let [or (μ (a b) (($ (φ False b) (φ x x)) a))]
        (let [xor (μ (a b) (($ (φ False b) (φ x (and ((not b) x)))) a))]
          (or ((not True) (and ((xor (True True)) True))))))))

and derive a runnable program in four rewrites, one per let:

> ((φ not
     ((φ and
        ((φ or
           ((φ xor
              (or ((not True) (and ((xor (True True)) True)))))
            (μ (a b) (($ (φ False b) (φ x (and ((not b) x)))) a))))
         (μ (a b) (($ (φ False b) (φ x x)) a))))
      (μ (a b) (($ (φ False False) (φ _ b)) a))))
   ($ (φ False True) (φ _ False)))

'False

This program calculates ¬True∨(TrueTrue)∧True = False with roughly the following trace:

    (or ((not True) (and ((xor (True True)) True))))
   (or (False (and ((xor (True True)) True))))
   (and ((xor (True True)) True))
   (and ((and ((Not True) True)) True))
   (and ((and (False True)) True))
   (and (False True))
   False

5.1.6.4 Lists

The list is a simple but useful algebraic data type. Given a nullary constructor Nil and a binary constructor Cons,

list

=

μ(x ◊).Cons(x;Nil);μ(x xs).Cons(x;list xs)

The list macro folds a ◊-terminated series of applications into a Nil-terminated series of Conses.

list

=

($ (μ (x ◊) (Cons ($ x Nil))) (μ (x xs) (Cons ($ x (list xs)))))

Using the hypothetical-to-runnable technique, we get:

> ((φ fix
     ((φ list
        (list ((Succ Zero)
               ((Succ (Succ Zero))
                ((Succ (Succ (Succ Zero)))
                 )))))
      (fix (φ list ($ (μ (x ) (Cons ($ x Nil)))
                      (μ (x xs) (Cons ($ x (list xs)))))))))
   (φ f
     ((φ x (f (φ y ((x x) y))))
      (φ x (f (φ y ((x x) y)))))))

'(Cons

  ($

   (Succ Zero)

   (Cons ($ (Succ (Succ Zero)) (Cons ($ (Succ (Succ (Succ Zero))) Nil))))))

This example merely constructs a list of the first three non-Zero Peano numbers.

Reversing lists is a little more interesting than constructing them.

reverse

=

φxs.rev(xs Nil)

rev

=

φ(Nil a).a;φ(Cons(x;xs) a).rev(xs Cons(x;a))

The reverse function takes a list xs and applies rev to it with a Nil initial accumulator a. The rev function then Conses non-Nil elements of xs onto a as it recursively calls itself on the tail of xs. Since a always holds a reversed copy of the non-Nil elements of xs rev has already seen, we can just return it when xs is Nil.

reverse

=

(φ xs (rev (xs Nil)))

rev

=

($ (φ (Nil a) a) (φ ((Cons ($ y ys)) a) (rev (ys (Cons ($ y a))))))

Again, we’ll find no surprises deriving a runnable example:

> ((φ fix
     ((φ list
        ((φ rev
           ((φ reverse
              (reverse (list ((Succ Zero)
                              ((Succ (Succ Zero))
                               ((Succ (Succ (Succ Zero)))
                                ))))))
            (fix (φ reverse (φ xs (rev (xs Nil)))))))
         (fix (φ rev
                ($ (φ (Nil a) a)
                   (φ ((Cons ($ y ys)) a) (rev (ys (Cons ($ y a))))))))))
      (fix (φ list ($ (μ (x ) (Cons ($ x Nil)))
                      (μ (x xs) (Cons ($ x (list xs)))))))))
   (φ f
     ((φ x (f (φ y ((x x) y))))
      (φ x (f (φ y ((x x) y)))))))

'(Cons

  ($

   (Succ (Succ (Succ Zero)))

   (Cons ($ (Succ (Succ Zero)) (Cons ($ (Succ Zero) Nil))))))

5.1.7 Closing Remarks

This concludes our first foray into interpreter construction with algebraic. In the next installment, we’ll extend the surface syntax for a more realistic look and feel.