Redex Miscellanea

8.12

Redex Miscellanea🔗ℹ

Cameron Moy

This library is under development; compatibility may not be maintained.

This package implements miscellaneous metafunctions, macros, and functions for Redex. For the purposes of illustration, we will use the following language in our examples.

(define-language Λ
  [e ::= x v (e e ...)]
  [v ::= (λ (x ...) e)]
  [x ::= variable-not-otherwise-mentioned]
  [E ::= hole (v ... E e ...)]

  #:binding-forms
  (λ (x ...) e #:refers-to (shadow x ...)))

(default-language Λ)

1 Metafunctions🔗ℹ

metafunction
(substitute-env target ([key value] ...))

Given an environment, a list of keys and values, replaces instances of key with value in the target term.

Example:

> (term (substitute-env x ([x 1] [y 2])))
1

metafunction
(substitute* target [key value] ...)

Shorthand for a call to substitute-env with the given key-value pairs as an environment.

Example:

> (term (substitute* x [x 1] [y 2]))
1

metafunction
(lookup ([key value] ...) needle)

Returns the first value whose key matches the needle. If none match, #f is returned.

Example:

> (term (lookup ([x 1] [y 2]) x))
1

metafunction
(ext ([key value] ...) [new-key new-value] ...)

Extends the given environment with the new key-value pairs, adding where the key isn’t already present, and overriding the value if the key is present.

Example:

> (term (ext ([x 1] [y 2]) [x 2] [z 3]))
'((z 3) (x 2) (y 2))

metafunction
(unique (any ...))

Returns whether the given elements are unique.

Examples:

> (term (unique (1 2 3)))
#t
> (term (unique (1 2 2)))
#f

metafunction
(rem ([key value] ...) old-key ...)

Removes the associations with the old-key if they are present in the environment. Does nothing otherwise.

Example:

> (term (rem ([x 1] [y 2]) x z))
'((y 2))

2 Macros🔗ℹ

syntax
(match-term lang expression [pattern expression] ...)

Matches the given term against a series of patterns, choosing the expression corresponding to the first matching pattern.

Example:

> (match-term Λ (term (λ (x) (x x)))
[(λ _ e) (term e)])
'(x«0» x«0»)

syntax
(not-match? lang pattern term)

Returns if the given pattern doesn’t match the term.

Examples:

> (not-match? Λ x (λ (y) y))
#t
> (not-match? Λ x y)
#f

syntax
(require-typed-primitives lang reduce-id type-id
maybe-convert-type
require-spec ...)

maybe-convert-type =
| #:convert-type convert-type-id

Thanks to Andrew Wagner for suggesting this feature.

Uses the given Typed Racket modules to define the reduction and typing of primitive operations. When specified, the type conversion procedure is given a datum representing the Typed Racket type, and is expected to return an equivalent type as a Redex term. Note, that you must define the type conversion function with define-syntax.

In the following, we import even?, odd?, and add1 from Typed Racket. Since add1 takes and returns arbitrary numbers, not just integers, we provide a type conversion function to handle the number type. This is because the object language only has integers.

(define-language Ω
  [e ::= v (e e ...)]
  [v ::= integer boolean o]
  [o ::= even? odd? add1]
  [E ::= hole (v ... E e ...)]

  [τ ::= Integer Boolean (-> τ τ ...)]
  [Γ ::= ([x τ] ...)])

(define-syntax (convert-type type)
  (let go ([type type])
    (match type
      ['Boolean (term Boolean)]
      ['Integer (term Integer)]
      ['Number (term Integer)]
      [`(-> ,x ...) (term (-> ,@(map go x)))])))

(require-typed-primitives
Ω δ Δ
#:convert-type convert-type
(only-in typed/racket/base add1 even? odd?))

(define-judgment-form Ω
  #:mode (⊢ I I I O)
  #:contract (⊢ Γ e : τ)
  [(⊢ Γ x : τ)
   (where τ (lookup Γ x))]
  [(⊢ Γ integer : Integer)]
  [(⊢ Γ boolean : Boolean)]
  [(⊢ Γ o : (Δ o))]
  [(⊢ Γ e_f : (-> τ_a ... τ_r))
   (⊢ Γ e_v : τ_a) ...
   ----------------------------
   (⊢ Γ (e_f e_v ...) : τ_r)])

(define ↦
  (reduction-relation
   Ω
   [--> (in-hole E (o v ...))
        (in-hole E (δ (o v ...)))
        δ]))

Given those definitions, we can now use those primitive operations.

Examples:

> (judgment-holds (⊢ () (even? 42) : Boolean))
#t
> (judgment-holds (⊢ () add1 : (-> Integer Integer)))
#t
> (apply-reduction-relation ↦ (term (even? 42)))
'(#t)
> (apply-reduction-relation ↦ (term (odd? 42)))
'(#f)
> (apply-reduction-relation ↦ (term (add1 42)))
'(43)

3 Functions🔗ℹ

procedure
(make-eval rr
[ #:inject inject
#:project project
#:program? program?
#:answer? answer?]) → (-> any/c any)
  rr : reduction-relation?
  inject : (-> any/c any) = values
  project : (-> any/c any) = values
  program? : predicate/c = (const #t)
  answer? : predicate/c = (const #t)

Returns an evaluation function that applies the given reduction relation until reaching a normal form. The evaluation function will inject into an initial machine configuration and project out of the final configuration. Initial and final expressions will be checked against program? and answer? respectively. The evaluation function takes a maximum of current-max-steps steps before aborting. Additionally it will throw an error on a non-deterministic or non-terminating result.

Examples:

> (define v
    (reduction-relation Λ
      [--> (in-hole E ((λ (x ..._a) e) v ..._a))
           (in-hole E (substitute* e [x v] ...))
           βv]))
> (define ⇓ (make-eval v))
> (⇓ (term ((λ (x) x) (λ (y) y))))
'(λ (y) y)

parameter
(current-max-steps) → natural?
(current-max-steps max-steps) → void?
max-steps : natural?
= 50

A parameter that determines the maximum number of steps the evaluation function created by make-eval will take before quitting.

Example:

> (⇓ (term ((λ (x) ((x x) x)) (λ (y) ((y y) y)))))
make-eval: exceeded maximum number of steps