►7400:   i  PPL (Spring 2020)
►Working with Redex
▼Lecture 1
►3 Redex, Quickly
On this page:
3.1 Languages and Term
3.2 Metafunctions
3.3 Testing
    ← prev  up  next → 

3 Redex, Quickly

3.1 Languages and Term

In Redex, you use define-language to specify the grammar of abstract syntax trees you wish to work on:
> (define-language Colors
    (c red
       yellow
       green))
A name such as c is known as a non-terminal, meaning it is a name for the trees enumerated on the right-hand side of the language clause. Items such as red are literal leaf elements of the collection of ASTs.

You can then use term to create terms from all kinds of Racket data, and you can use define to give these terms a name.
> (term yellow)

'yellow

Technically, (term yellow) creates the Racket symbol 'yellow. Because Redex is a Racket-hosted domain-specific language, you occasionally need to understand this relationship. It also implies that you can use other Racket features on occasion, such as define for giving (variable) names to terms:
> (define example1 (term yellow))
> example1

'yellow

> (define example2 (term green))
> (define example3 (term brown))
The second interaction shows that the placeholder example1 truly stands for 'yellow.

In general, the way to understand a language definition is to see it as a recipe for generating tree-shaped values, in our domain called terms. In this light the Colors language says that the class of c terms consists of three values: red, yellow, green.

Clearly there is nothing tree-structured about Colors, so consider a somewhat more interesting definition:
(define-language ArithmeticExpressions
  (e n
     (e + e)
     (e * e))
  (n number))
The definition of e in ArithmeticExpression is self-referential or recursive. Such definitions should make you nervous because they could be nonsensical—even if you are not a mathematician who says a defined term must be replaceable with its definition in all contexts. The only way to show that this self-referential definition makes sense is to enumerate the member of the class to show that it exists:

  • Obviously the first line of e’s definition says that all ns belong to e. Since (term 1) is a number, it is an e. Yeah! The class of es isn’t empty.

  • Now the second like is a bit weirder. We know that + is meant to be the literal symbol. So what this means is that we need to find two es: one to put on the left side and one on the right. Lucky us, we have a proof that 1 belongs to e, so
    > (term (1 + 1))

    '(1 + 1)

    belong to e, too. If you draw (term (1 + 1)) as a tree, you get this simple image:

    image

    As always in CS, we draw trees upside down.

  • As you may have guessed, you can use the new-found (1 + 1) to generate an even larger e, namely,
    > (term ((1 + 1) + 1))

    '((1 + 1) + 1)

    for example. What you see from this interaction is that Redex uses Racket’s S-expressions to represent such terms. The tree for this second term is deeper and more complex than the first one:

    image

    Even though it too looks simple, you should now be able to understand why we call our terms “trees” and soon you will appreciate why we imagine trees when we process terms.

And now that you have the hang of it, you can generate as many e terms as you want. As it turns out, almost all programming languages that we wish to model have such self-referential definitions, but for now we return to simpler definitions to grow your familiarity with define-language and other Redex features.

With redex-match you can find out whether a term belongs to a specific category of trees in a language:
> (redex-match Colors c example1)

(list (match (list (bind 'c 'yellow))))

> (redex-match Colors c example2)

(list (match (list (bind 'c 'green))))

> (redex-match Colors c example3)

#f

It answers with with a list of possible matches if so; otherwise, it produces #f (for false).

3.2 Metafunctions

To process terms in a language, you define metafunctions in the context of a specific language:
> (define-metafunction Colors
     successor : c -> c
     [(successor red) green]
     [(successor green) yellow]
     [(successor yellow) red])
Here successor is defined for the Colors language from above. The first line states an optional contract, which says that successor is a function that consumes c trees and produces them. The remaining clauses, enclosed in brackets, specify which call produces which result.

A metafunction must be called in a term context:
> (term (successor yellow))

'red

> (term (successor brown))

successor: (successor brown) is not in my domain

The first calls produces a term—displayed with Racket’s quote or ' notation. The second call signals a contract violation. Note that contracts are checked at run-time, i.e., when DrRacket evaluates a call to the function not when the function is compiled.

3.3 Testing

While DrRacket’s interaction area is a good medium for exploring programs, it is not a suitable tool for testing programs. A unit test in Redex consists of a function call and an expected result, sometimes a term, sometimes a Racket value, say a number:
> (test-equal (term (successor red)) (term green))
> (test-equal (term (successor red)) (term red))

FAILED :5.0

  actual: 'green

expected: 'red

Successful tests check quietly; failing tests signal a problem and stop the program.

    ← prev  up  next →