6.10.0.2
3 Modeling Functional Expression Languages
Goals |
— |
— |
— |
3.1 Dealing with Terms and Syntax
Let’s step back and look at language modeling slowly.
After you have a syntax, use the grammar to generate instances and check
them (typos do sneak in). Instances are generated with term:
(define e1 (term y)) (define e2 (term (lambda (y) y))) (define e3 (term (lambda (x) y))) (define e4 (term (,e2 ,e3)))
Mouse over define. It is not a Redex form, it comes from
Racket. Take a close look at the last definition. Comma anyone? Enter
e4 at the REPL and see what it says.
How about checking whether a term belongs to a syntactic category in a
language?
(redex-match? Lambda e e4)
Define yourself a predicate that tests membership:
(define Lambda? (redex-match? Lambda e))
Now you can formulate language tests:
(test-equal (Lambda? e1) #true) (test-equal (Lambda? e2) #true) (test-equal (Lambda? e3) #true) (test-equal (Lambda? e4) #true) (define eb1 (term (lambda (x x) y))) (define eb2 (term (lambda (x) 3))) (test-equal (Lambda? eb1) #false) (test-equal (Lambda? eb2) #false) (test-results)
Make sure your language contains the terms that you want and does
not contain those you want to exclude. Why should eb1 and
eb2 not be in Lambda’s set of expressions?
3.2 Meta-functions
Rule Avoid escaping to Racket. Racket is a general-purpose language, and Redex is a language about terms.
But, language models need meta-functions in addition to reduction relations. We have seen one such function in action: substitute. It is a meta-function, i.e., a function that maps terms to terms. It is a bit unusual, because it is also needs to be told (via default-language) which language to deal with.
Whenever Redex encounters the use of a meta-function in a term context, it evaluates it automatically. It does not need any extra hints.
Language modelers want to define their own meta-functions. Here is the
name-giving example:
Remember that the right-hand side of a relation is a term position. When
Redex finds the application of a meta-function there, it evaluates it. So
now we need to define the meta-function plus to get PCF back:
(define-metafunction PCF-eval plus : n n -> n [(plus 1 1) 2] [(plus n n) 3] [(plus n_1 n_2) 1])
A meta-function is specified via pattern matching. The right-hand side
of each case is a term context. Just like for reduction relations,
we could escape to Racket via a comma (unquote).
This might not be what you had in mind, but nobody said PCF’s number system is the one from Racket. As a matter of fact, it is not.
A second example is a function that helps Falsify your language. Let’s say
we want ff and 0 to stand for false. We could add
another reduction rule or we could use a meta-function to express the idea
that if coerces the test value:
(--> (in-hole E-name (if v e_1 e_2)) (in-hole E-name e_1) (where tt (falsify v)) if-tt) (--> (in-hole E-name (if v e_1 e_2)) (in-hole E-name e_2) (where ff (falsify v)) if-ff)
The where clause imposes a side condition on the relation. Its
right-hand side is a term position; if Redex finds the application of a
meta-function there, it evaluates it.
Here is the obvious definition of falsify:
(define-metafunction PCF-eval falsify : v -> tt or ff [(falsify 0) ff] [(falsify ff) ff] [(falsify v) tt])
A final example is eval:
(define-metafunction Lambda-calculus eval : e -> v [(eval e) ,(first (apply-reduction-relation* ->name (term e)))])
Ouch, we just escaped to Racket. Let’s reduce the use of Racket:
(define-metafunction Lambda-calculus eval-1 : e -> v [(eval-1 e) v (where (v) ,(apply-reduction-relation* ->name (term e)))])
But look what happens if we use eval on (y (lambda (x) x)). It blows up; the codomain test fails. Going back to Plotkin’s seminal paper (1974), nobody uses terms with free variables as programs. So, we want a definition of eval that fixes this. This needs two things: (1) side-conditions on clauses and (2) a function that retrieves the free variables from a term.
Here is how we do the first step:
(define-metafunction Lambda-calculus eval-2 : e -> v or (unbound-variables (x ...)) [(eval-2 e) v_one-term (where () (fv e)) (where (v_one-term) ,(apply-reduction-relation* ->name (term e)))] [(eval-2 e) (unbound-variables (fv e))])
The function has two clauses now. The first one is protected with two
where constraints: the first one ensures e is closed and
the second one checks that reducing e produces only one
result. The second clause of eval-2 ignores the input and signals
a “compile-time” error.Compilers often call this
“undefined variable.”
From the context, we can guess that fv retrieves the list of free
variables from a term e. So this is its header:
; retrieve the list of free variables from e (define-metafunction Lambda-calculus fv : e -> (x ...))
The function traverses e in a syntax-directed manner of course:
; retrieve the list of free variables from e (define-metafunction Lambda-calculus fv : e -> (x ...) [(fv x) (x)] [(fv (lambda (x) e)) (minus (fv e) x)] [(fv (e_1 e_2)) (union (fv e_1) (fv e_2))])
If you have ever seen such a function before, you know that this is very
much standard—
For union, we cheat:
(define-metafunction Lambda-calculus union : (x ...) (x ...) -> (x ...) [(union (x_1 ...) (x_2 ...)) (x_1 ... x_2 ...)])
For minus, we show off a cool feature of Redex pattern matching:
(define-metafunction Lambda-calculus minus : (x ...) x -> (x ...) [(minus (x_1 ... x x_2 ...) x) (minus (x_1 ... x_2 ...) x)] [(minus (x_1 ...) x) (x_1 ...)])
3.3 Testing
But we really want test-driven development of these
functions. Here is how:
(test-equal (term (minus () x)) (term ())) (test-equal (term (minus (x) x)) (term ())) (test-equal (term (minus (x y) x)) (term (y))) (test-equal (term (minus (z w x y) x)) (term (z w y)))
If you want to develop tests before you code, or if you want to illustrate
functions with tests before people read the code, use (module+ test ...).
And we want tests for our reduction relations:
The first succeeds using alpha-equivalent? implicitly; the second
fails (as expected). The test-->> form tests the transitive closure
of the relation.