Programming Language Design

Theory of Programming Languages

Learning Objectives

  • You know where to find supplementary material for programming language theory.
  • You know some of the common notation used in programming language theory, such as inference rule and evaluation notation.
  • You know how inference rules are used to define the relations between different constructions in programming languages.
  • You know how formation trees are used to define abstract data types.
  • You know how a simple proof of an evaluation relation is constructed.

Introduction

Classically, the study of programming languages is split into syntax and semantics, where syntax refers to the grammar and the syntactic rules of the language, whereas semantics refers to the meaning and validity of sentences in the language. However, modern theory has moved on from studying the formal structure into something more abstract where programs are considered to be mathematical objects governed by statics and dynamics.

  • Statics define features of the programming language, such as how terms and programs are formed and how the terms are typed.
  • The dynamics define how these features behave at “runtime”, i.e. during evaluation or execution. The dynamics can rely on the invariants placed by the statics, such as “variable x is an integer”, to provide safe (and usually deterministic) behavior for the programs.

A well designed programming language usually shifts weight to the statics of the language, as its properties are (closer to being) mathematically provable. Well designed programs in these languages use the statics (mostly the type system) to bear more of the weight of the business logic1 so that you get the feeling that “if it compiles, it works”2. Very few programming languages actually manage to cross this “line of confidence” — and those which do, the author claims, have strong type systems.

Loading Exercise...

For a more thorough look at programming language theory, have a look at the following textbooks

  • Types and Programming Languages by Benjamin C. Pierce.

    A thorough and approachable book that covers almost all currently relevant programming language properties. This book was the primary inspiration for this whole course.

  • Practical Foundations for Programming Languages by Robert Harper.

    A bit more logically thorough approach to programming languages than Types and Programming Languages. The notation and terminology used on this course closely matches this book.

  • Essentials of Programming Languages by Friedman and Wand (free).

    A very concrete approach to designing programming languages. The book uses scheme, a member of the LISP programming language family, for all of the implementatino code.

  • Introduction to the Theory of Programming Languages by Bertrand Meyer (free).

    Covers all the basics very thoroughly and uses a common knowledge concepts for examples.

  • Programming Language Foundations (free).

    A one hundred percent formalized and machine-checked book about developing the simply typed lambda calculus from scratch using a proof assistant.

The most approachable textbook is Types and Programming Languages (in the author’s opinion) after which the next logical step is Practical Foundations for Programming Languages

All of these resources are recommended supplementary reading, but understanding the theory of programming languages thoroughly is not required on this course.

Programming, Formal Systems and Logic

Programming languages were mostly studied through formal systems with an underlying logical system. Logic and computation remained mostly separate until the logicians Haskell Curry and William Howard realized that code and mathematics are deeply connected.

Nowadays programming languages are not only studied through meta-theories based on logic, but are also used as a foundations of mathematics1 to study other programming languages2 or even areas of mathematics3!

FormalsystemsFormal languages, BNF,finite automataDeductivesystemsWell-formedformulasNonsenseMathematicalproofsAxiomsRules ofinferenceFig 1. — Relationship between areas of formal systems and languages.

Inference Rules

The logical notation used and developed in this chapter is at least somewhat standard in programming language (and mathematical) literature.

Inference rules, also known as transformation rules, are a construction from formal logic which allows us to clearly express the rules governing relations. Inference rules consist of a set of premises and a conclusion and when written down, the premises and conclusion are visually separated by a horizontal line. The premises and conclusion are judgments which could be thought of as “statements”.

For example, the premises 𝐴→𝐵 and 𝐴 could be transformed into the conclusion 𝐵, for any well-formed4 propositions 𝐴,𝐵. This inference rule is commonly known as modus ponens and can be visually written as:

𝐴→𝐵𝐴𝐵

The 𝐴 and 𝐵 and possibly other variables present in inference rules are called metavariables and they can be replaced with anything that meets the “type signature” of the surrounding operators and relations.

For extra reading, see Introduction to the Theory of Programming Languages, Chapter 9.2.6.

Loading Exercise...

Formation Rules

A formal language is divided into nonsense and well-formed formulas.

True-FTrue:TermFalse-FFalse:Term𝑡1:Term𝑡2:Term𝑡3:TermIte-FIte(if:𝑡1,then:𝑡2,else:𝑡3):Term

The suffix “-F” refers to a formation rule.

E.g. the term Ite(if:True,then:False,else:True) has the following formation tree:

True-FTrue:TermFalse-FFalse:TermTrue-FTrue:TermIte-FIte(if:True,then:False,else:True)
Loading Exercise...

Evaluation Rules

Evaluation rules will be used to analyze the dynamics5 of programming languages. The word dynamics refers to how the language behaves during evaluation or “execution” — it is unrelated to the concept of dynamic programming languages or dynamic programming.

An evaluation rule is simply a relation between a term and a value. The reason we want a relation is that evaluation is not always a function. For example a random number generator is non-deterministic, and therefore not functional, but it still is a relation and we can reason about the outcomes in a mathematical way.

We can turn the eval function from chapter 4 into a relation very easily, so let’s do that now and define a relation (⇓) for our arithmetic language:

The double arrow pointing down is often used when defining big-step operational semantics for a language.

Definition 4.5.1: Evaluation relation (⇓)Let 𝑡:Term and 𝑛:ℤ. The evaluation relation (⇓) is a binary relation,such that 𝑡⇓𝑛 if and only if eval(𝑡)=𝑛. Example 4.5.2: Evaluation relation (⇓)The following propositions are true:1.Num(1)⇓1.2.Add(Num(1),Num(2))⇓3.3.Sub(Num(1),Mul(Num(2),Num(3)))⇓−5.4.∀𝑛:ℤ,Num(𝑛)⇓𝑛,   i.e. all terms Num(𝑛) evaluate to 𝑛.5.∀𝑚:ℤ,𝑚≠1⇒¬(Num(1)⇓𝑚),   i.e. Num(1) does not evaluate toany number 𝑚≠1.

Let’s spell out the evaluation rule for Num(𝑛):

Num(𝑛)⇓𝑛

This is read as: “under no assumptions, Num(𝑛) evaluates to 𝑛.”

This rule can be instantiated for any value of the metavariable 𝑛:ℤ, meaning that all the following evaluation rules exist:

…Num(−1)⇓−1Num(0)⇓0Num(1)⇓1…
Loading Exercise...

Next, let’s think about what the evaluation rule for Add looks like. Let’s start with the conclusion — we want to express that addition evaluates to the sum of the values that the subterms evaluate to. Call these values 𝑛1 and 𝑛2, and we can conclude (under the to be determined assumptions)

Add(𝑡1,𝑡2)⇓𝑛1+𝑛2.

Well it’s quite simple to see that the assumption should say something about 𝑡1 and 𝑛1 or otherwise the evaluation rule would conclude that any 𝑡1 evaluates to any 𝑛1. The reasonable assumptions would therefore be 𝑡1⇓𝑛1 and 𝑡2⇓𝑛2 and we get:

𝑡1⇓𝑛1𝑡2⇓𝑛2Add(𝑡1,𝑡2)⇓𝑛1+𝑛2

Again, we can think of 𝑡1,𝑡2,𝑛1,𝑛2 as metavariables which can be replaced with any value of the appropriate type. For example an instance of the evaluation rule could be:

Num(1)⇓5Num(2)⇓8Add(Num(1),Num(2))⇓5+8

Which reads: “if Num(1) evaluates to 5 and Num(2) evaluates to 8, then Add(Num(1),Num(2)) evaluates 5+8.”

This is of course logically valid, even though the assumptions are false in this case as Num(1)⇓5 doesn’t hold. Here we see how the assumptions are a way to constrain the values of the metavariables 𝑡1,𝑡2,𝑛1,𝑛2 so that some relations hold between them.

Finally, the evaluation rules for Sub and Mul are similar:

𝑡1⇓𝑛1𝑡2⇓𝑛2Sub(𝑡1,𝑡2)⇓𝑛1−𝑛2𝑡1⇓𝑛1𝑡2⇓𝑛2Mul(𝑡1,𝑡2)⇓𝑛1⋅𝑛2

It’s very important to note that these are all the rules for evaluation (for this language), or the evaluation relation is the closed under these rules. This means that we can say exactly which rule was/is used during evaluation.

Loading Exercise...

Proof Trees

Tying all of this together, we can examine how the evaluation rules determine the value of a term. Let’s start with e.g. Add(Num(1),Mul(Num(2),Num(3))). Our goal is to construct a proof tree using the evaluation rules, such that at the top of the tree, there are no explicit assumptions left.

A proof tree shows the complete picture of every evaluation rule used to form the statement. Proof trees are not only about mathematical propositions — they can also be used to describe how a sentence in some grammar is constructed according to BNF derivation rules (called formation rules in formal logic).

First, to match the evaluation rule for Add, we need to replace 𝑡1 by Num(1) and 𝑡2 by Num(2).

Num(1)⇓𝑛1Mul(Num(2),Num(3))⇓𝑛2Add(Num(1),Mul(Num(2),Num(3)))⇓𝑛1+𝑛2

We leave the values 𝑛1,𝑛2 as metavariables hoping that we find a value for them later.

Next, we need to create subtrees for both of the assumptions. Which rule matches Num(1)? The Num rule!

In order to use the rule, we simply draw a horizontal line over both Num(1)⇓𝑛1.

Our proof tree is not yet finished as there are assumptions left. The assumption Mul(Num(2),Num(3))⇓𝑛2 needs a proof of its own. Here we should use the Mul rule, but 𝑛2 doesn’t look like a multiplication… This is in fact not a problem, we introduce two new metavariables 𝑚1,𝑚2 (yes we can do that) and say 𝑛2=𝑚1⋅𝑚2. Now we can just write 𝑛2 as a multiplication of the two integers.

Here is the incomplete proof tree for Mul(Num(2),Num(3))⇓𝑛2:

Num(2)⇓𝑚1Num(3)⇓𝑚2Mul(Num(2),Num(3))⇓𝑚1⋅𝑚2

Now we just prove both assumptions using the Num rule:

Num(2)⇓𝑚1Num(3)⇓𝑚2Mul(Num(2),Num(3))⇓𝑚1⋅𝑚2

Putting the proofs together and replacing 𝑛2 with 𝑚1⋅𝑚2, we get a tree that looks like this:

Num(1)⇓𝑛1Num(2)⇓𝑚1Num(3)⇓𝑚2Mul(Num(2),Num(3))⇓𝑚1⋅𝑚2Add(Num(1),Mul(Num(2),Num(3)))⇓𝑛1+(𝑚1⋅𝑚2)

The only thing left is to replace 𝑛1 by its value 1, 𝑚1 by 1 and 𝑚2 by 2, resulting in:

Num(1)⇓1Num(2)⇓2Num(3)⇓3Mul(Num(2),Num(3))⇓2⋅3Add(Num(1),Mul(Num(2),Num(3)))⇓1+(2⋅3)

The reason every step worked out so smoothly was because of the fact that our relation was defined using a function (a functional and total relation). This fact made every subtree uniquely determined (by functionality) and ensured there was at least one evaluation rule we could use to progress the subtree (totality).

Loading Exercise...
Loading Exercise...

Footnotes

Footnotes

  1. Idris, a language for type driven development, type safe zero-cost abstractions in Rust ↩ ↩2

  2. Rust users forum Haskell Wiki ↩ ↩2

  3. Annals of Formalized Mathematics, a journal that publishes articles about formalized mathematics and mathematical applications of proof assistants. ↩

  4. Well-formed means that the formula is syntactically valid, i.e. derived from the formation rules of the language of propositional logic. ↩

  5. See Practical Foundations for Programming Languages, chapters 5 and 7. ↩

← Building a Calculator
Boolean Expression Language →