►7400:   i  PPL
►Working with Redex
▼Lecture 1
    ← prev  up  next → 

2 Programming Languages

For Java, the specification document spells out both the lexical structure (vocabulary) and the syntax (grammar) with a mixture of structured English and formal enumerations. Take a look at the specifications to see how much care and work goes into an exemplary language specification.

Given Java’s grammar, you can check whether a phrase such as

  class Fahrenheit {

   private double temperature = 0.0;

   public Celsius toCelsius() {

     return 5 * (this.temperature - 32) / 9;

   }

  }

belongs to the language that the grammar describes. But, is this phrase truly different from
(define Fahrenheit
  (class object% [init-field (temperature 0.0)]
     (define/public (toCelsius)
        (/ (* 5 (- temperature 32)) 9))))
Or does a phrase such as

  x = x + 1;

really mean something radically different than

(set! x (+ x 1))

Since programming language researchers wish to ignore such syntactic differences and focus on models that predict behavior (semantics), they distill syntax to its essence: abstract syntax. Roughly speaking, the elements of an abstract syntax are trees that explain why an element belongs to the language. That is, the tree structure encapsulates the argument why a grammar such as Java’s “blesses” a sentence such as the class definition about.

So in order to study syntax and semantics we need:

  1. a tool for writing down abstract syntax trees;

  2. a tool for writing down functions on abstract syntax trees to check basic properties.

In this course, we use Redex for this purpose. Redex languages are what we use for the first point and Redex metafunctions are executable specifications of mathematical functions on languages. This lecture and the next few introduce Redex and also how to prove theorems about Redex languages and metafunctions.

    ← prev  up  next →