### 1` `Preface—Why Redex

a collection of expressions,

with an evaluation function (relation),

which satisfy some properties.

This is not the only definition, and might not be the best definition, but it’s a definition that works for me.

What I want out of a programming language modeling tool is the ability to model these pieces of the language, and use the tool to check my own intuitions and reasoning. The tool ought to match my own intuitions about a language, and the tool ought to communicate in the same abstractions as I do.

Is this syntax a valid expression in the language?

Is this syntax a valid value in the language?

Does this expression decompose into a context and this other expression in the hole?

Does this expression evaluate to some value?

Does some other expression evaluate to the same value?

Do all expressions evaluate?

Do all expressions evaluate to a value?

Does this expression have this property?

Do all expressions of this form have this property?

The reason I prefer Redex is that (1) Redex and I agree about what a language is and (2) I can very quickly get a model and start asking Redex these questions. Redex imposes few restrictions, and tries hard to do something useful. One of the authors of Redex described it as "a scripting language for metatheory".

I pick on Coq because it’s another tool I know fairly well and sometimes use.

>

`Parameter Var : Type.`

`Var is declared`

>

`Inductive BoxyType : Type :=`

| boxy_ty_nat : BoxyType

| boxy_ty_box : BoxyType -> BoxyType

| boxy_ty_fun : BoxyType -> BoxyType -> BoxyType

| boxy_ty_pair : BoxyType -> BoxyType -> BoxyType.`BoxyType is defined`

BoxyType_rect is defined

BoxyType_ind is defined

BoxyType_rec is defined

BoxyType_sind is defined>

`Inductive BoxyTerm : Type :=`

| boxy_tm_nat : nat -> BoxyTerm

| boxy_tm_var : Var -> BoxyTerm

| boxy_tm_cons : BoxyTerm -> BoxyTerm -> BoxyTerm

| boxy_tm_car : BoxyTerm -> BoxyTerm

| boxy_tm_cdr : BoxyTerm -> BoxyTerm

| boxy_tm_plus : BoxyTerm -> BoxyTerm -> BoxyTerm

| boxy_tm_fun : Var -> BoxyType -> BoxyTerm -> BoxyTerm

| boxy_tm_app : BoxyType -> BoxyTerm -> BoxyTerm

| boxy_tm_box : BoxyType -> BoxyTerm

| boxy_tm_unbox : Var -> BoxyType -> BoxyTerm -> BoxyTerm.`BoxyTerm is defined`

BoxyTerm_rect is defined

BoxyTerm_ind is defined

BoxyTerm_rec is defined

BoxyTerm_sind is defined>

`Inductive BoxyValue : BoxyTerm -> Prop :=`

| boxy_v_nat : forall n, BoxyValue (boxy_tm_nat n)

| boxy_v_box : forall e, BoxyValue (boxy_tm_box e)

| boxy_v_fun : forall x t e, BoxyValue (boxy_tm_fun x t e)

| boxy_v_cons : forall v1 v2, BoxyValue v1 -> BoxyValue v2 -> BoxyValue (boxy_tm_cons v1 v2).`BoxyValue is defined`

BoxyValue_ind is defined

BoxyValue_sind is defined

This defines the syntax for a simply-typed λ-calculus with the box modality in Coq.

It leaves the type Var of variables abstract, for reasons anyone familiar with modeling languages in Coq will understand.

>

`Example example1 : BoxyTerm := boxy_tm_nat 1.`

`example1 is defined`

Even when I write out terms, I cannot easily ask whether a term matches some other nonterminal, e.g., I cannot ask whether the above term is a value. I can only prove that it is, and perhaps fail, or I must write a decision procedure.

>

`(* Is example1 a value? *)`

Lemma example2 : (BoxyValue example1).`1 goal (ID 12)`

============================

BoxyValue example1>

`Proof.`

>

`auto.`

>

`Qed.`

`Toplevel input, characters 1-5:`

> Qed.

> ^^^^

Error: (in proof example2): Attempt to save an incomplete proof>

`(* Well I dunno. I guess I have to prove it by hand. *)`

Fixpoint is_value (e : BoxyTerm) : bool :=

match e with

| boxy_tm_box e' => true

| boxy_tm_nat n => true

| boxy_tm_fun x A e => true

| boxy_tm_cons e1 e2 => andb (is_value e1) (is_value e2)

end.`Toplevel input, characters 58-252:`

> Fixpoint is_value (e : BoxyTerm) : bool :=

> match e with

> | boxy_tm_box e' => true

> | boxy_tm_nat n => true

> | boxy_tm_fun x A e => true

> | boxy_tm_cons e1 e2 => andb (is_value e1) (is_value e2)

> end.

Error: Non exhaustive pattern-matching: no clause found for pattern

boxy_tm_var _>

`(* Oops *)`

Fixpoint is_value (e : BoxyTerm) : bool :=

match e with

| boxy_tm_box e' => true

| boxy_tm_nat n => true

| boxy_tm_fun x A e => true

| boxy_tm_cons e1 e2 => andb (is_value e1) (is_value e2)

| _ => false

end.`is_value is defined`

is_value is recursively defined (guarded on 1st argument)>

`Eval compute in (is_value example1).`

`= true`

: bool

And that is just to deal with syntax.

I cannot quickly formalize the reduction systems, and when I do, I again have to manually compile it into Coq’s type theory (to get the small-step relational presentation I prefer), or into a fuel monad (to get a version that actually computes). It would take me hours and 100s of lines of code to define the full model and get to a point where I can ask the questions I want to ask.

If this were the state-of-the-art, I wouldn’t bother to use a computer for experimenting with languages. It costs me much more time to come up with the model than to work on paper. Trying to implement that model is completely unintuitive. I end up struggling with details, like how I represent variables, that have nothing to do with the problem I’m trying to solve. The only time I would use that technique, if ever, is if I were writing high-assurance software with lives on the line, or if I really needed to convince reviewers to accept my paper.

As I will show in the rest of this tutorial, with Redex, I can go from nothing to a model that computes in minutes and 10s of lines of code. A Redex model is nearly identical to what I write on paper, so it’s almost completely intuitive (assuming a formal programming languages background). Redex tries hard to do what you mean, which is what I want when experimenting. I save a ton of time by letting Redex generate and check examples, and run the computations. It’s not a replacement for a proof assistant, but it’s irreplaceable for experimenting.

So how do I use Redex to experiment?