Awesome

PLT Redex models of LVar calculi

Subdirectories include:

lambdaLVish: a Redex model of the lambdaLVish calculus that appears in my 2015 dissertation (see README).
LVish: a PLT Redex model of the LVish calculus that appears in our POPL 2014 paper and accompanying tech report (see README).
lambdaLVar: a PLT Redex model of the lambdaLVar calculus that appears in our FHPC 2013 paper and accompanying tech report (see README).

Modeling lattice parameterization in Redex, or, writing macros that write Redex models

All the LVar calculi have stores containing "lattice variables", or LVars. An LVar is a mutable store location whose contents can only increase over time, where the meaning of "increase" is given by a partially ordered set, or lattice, that the user of the language specifies. Different instantiations of the lattice result in different languages.

In the Redex of today, it's not possible to parameterize a language definition by a lattice (see discussion here). So, instead, for each one of these Redex models we define a Racket macro that takes a lattice as one of its arguments and generates a Redex language definition.

`define-lambdaLVar-language`

For lambdaLVar, this macro is called define-lambdaLVar-language. It takes the following arguments:

a name, e.g., lambdaLVar-nat, which becomes the lang-name passed to Redex's define-language form.
a lub operation, e.g., max, a Racket-level procedure that takes two lattice elements and returns a lattice element.
some number of Redex patterns representing lattice elements, not including top and bottom elements, since we add those automatically. (Therefore, if we wanted a lattice consisting only of Top and Bot, we wouldn't pass any lattice elements to define-LVish-language.)

For instance, to generate a language definition called lambdaLVar-nat where the lattice is the natural numbers with max as the least upper bound, one can write:

(define-lambdaLVar-language lambdaLVar-nat max natural)

Here natural is a pattern built into Redex that matches any exact non-negative integer.

The file lambdaLVar/nat.rkt contains this instantiation and a test suite of programs for lambdaLVar-nat. lambdaLVar/natpair.rkt and lambdaLVar/natpair-ivars.rkt contain two more example instantiations.

`define-LVish-language`

For LVish, this macro is called define-LVish-language. It takes the following arguments:

a name, e.g., LVish-nat, which becomes the lang-name passed to Redex's define-language form.
a "downset" operation, a Racket-level procedure that takes a lattice element and returns the (finite) set of all lattice elements that are below that element. The downset operation is used to implement the freeze ... after ... with primitive in LVish.
a lub operation, a Racket-level procedure that takes two lattice elements and returns a lattice element.
some number of Redex patterns representing lattice elements, not including top and bottom elements, since we add those automatically.

For instance, to generate a language definition called LVish-nat where the lattice is the natural numbers with max as the least upper bound, one can write:

(define-LVish-language LVish-nat downset-op max natural)

where natural is a Redex pattern, as described above, and downset-op is defined as follows:

(define downset-op
  (lambda (d)
    (if (number? d)
        (append '(Bot) (iota d) `(,d))
        '(Bot)))))

The file LVish/nat.rkt contains this instantiation and a test suite of programs for LVish-nat. LVish/natpair-ivars.rkt contains another example instantiation.

`define-lambdaLVish-language`

For lambdaLVish, this macro is called define-lambdaLVish-language. It takes the following arguments:

a name, e.g., lambdaLVish-nat, which becomes the lang-name passed to Redex's define-language form.
a "downset" operation, a Racket-level procedure that takes a lattice element and returns the (finite) set of all lattice elements that are below that element.
a lub operation, a Racket-level procedure that takes two lattice elements and returns a lattice element.
a list of update operations, Racket-level procedures that each take a lattice element and return a lattice element.
some number of lattice elements represented as Redex patterns, not including top and bottom elements, since we add those automatically.

For instance, to generate a language definition called lambdaLVish-nat where the lattice is the non-negative integers ordered in the usual way, and there are two update operations which respectively increment the contents of an LVar by one and two, one could write:

(define-lambaLVish-language lambdaLVish-nat downset-op max update-ops natural)

where natural and downset-op are as above, and update-op is defined as follows:

(define update-op-1
  (lambda (d)
    (match d
      ['Bot 1]
      [number (add1 d)])))

(define update-op-2
  (lambda (d)
    (match d
      ['Bot 2]
      [number (add1 (add1 d))])))

(define update-ops `(,update-op-1 ,update-op-2))

The file lambdaLVish/nat.rkt contains this instantiation and a test suite of programs for lambdaLVish-nat.

Reduction traces

One nice feature that Redex offers is the ability to see a graphical "trace" of the reduction of a term (that is, the running of a program) in DrRacket. In order to use the trace feature with one of these Redex models, you have to first instantiate the model with a lattice. Open the file for the instantiation you want to use (such as "nat.rkt"), and click the "Run" button to open a REPL. Then, in the REPL:

(require (submod "." language)). This will bring the definition of the reduction relation into scope.
(require redex). This will bring traces into scope.
Try tracing a term with the traces command: (traces <rr> <term>) where <rr> is the reduction relation and <term> is some term in your instantiation of the model. For example, for the language defined in "nat.rkt", you can try:

(traces rr (term
            (()
             (let ((x_1 new))
               (let par
                   ((x_2 (puti x_1 1))
                    (x_3 (puti x_1 2)))
                 (freeze x_1)))))

This will open a window showing a reduction graph.