12/4/18: The Path Forward

We took a quick look today at the Nat-Nat problems, and in particular around the distinction between + and plus. But the main conversation was over what to do next quarter. The current plan is some combination of learning linear logic (anyone know of great references?!) and blodwen, as the later makes (or at least, is demonstrated to make, which isn't quite the same thing) effective use of linearity constraints in its types.

Blodwen & Agda

A couple of interesting tweets came out over the weekend, referring to new resources on the web.

Blodwen

The first is a Code Mesh talk given by Edwin Brady on Blodwen, a.k.a., Idris 2. Among Blodwen's more interesting capabilities: improved program inference, and linear types. These interact in a fascinating way: using program inference to implement the function

	transform : Vect m (Vect n A) -> Vect n (Vect m A)

“succeeds” in writing type-correct, but semantically incorrect code. Adding a one-use constraint in blodwen inferring code which is both type- and semantics-correct.

Programming Language Foundations in Agda

The second is the publication of the web-based textbook Programming Language Foundations in Agda by Philip Wadler and Wen Kokke.

Nat-Nat Problems

Problem 1. Write the functions max and monus, where

    (claim max
      (-> Nat Nat Nat))

is the usual max function, e.g.,

    > (max 3 7)
    (the Nat 7)

and where

    (claim monus
      (-> Nat Nat Nat))

is zero-truncated subtraction, e.g.,

    > (monus 7 3)
    (the Nat 4)
    > (monus 3 7)
    (the Nat 0)

Problem 2. The max and min definitions (along with the max-monus-theorem) follow a similar programming pattern in defining a binary function on Nat via a recursion on both arguments simultaneously. Define a function rec-Nat-Nat that captures this recursion, and use it to give alternative definitions of max and monus along with min and diff, where diff gives the distance between two Nats, e.g.,

    > (diff 7 3)
    (the Nat 4)
    > (diff 3 7)
    (the Nat 4)

Problem 3. Prove the following theorem relating max and monus:

    (claim max-monus-theorem
        (Pi ((m Nat)
             (n Nat))
            (= Nat (max m n) (+ m (monus n m)))))

Note: This is a hard problem, and requires persistence and planning.

Problem 4. The emergence of rec-Nat-Nat raises an intriguing possibility. The proof of the commutativity of + typically requires first proving a couple of theorems that essentially symmetrize it, i.e.,

    (claim +zero
        (Pi ((m Nat))
            (= Nat (+ m 0) m)))

and

    (claim +succ
        (Pi ((m Nat)
             (n Nat))
            (= Nat (+ m (add1 n)) (add1 (+ m n)))))

An attractive possibility is to define plus via rec-Nat-Nat, an alternative definition of addition which is already symmetric, based on the following equations for addition:

    0 + 0 = 0
    m + 0 = m
    0 + n = n
    (m+1) + (n+1) = 2 + (m+n)

With this definition, the hard case of proving commutativity is in showing that if

    m + n = n + m

then

    (m+1) + (n+1) = (n+1) + (m+1).

But this is easy to argue directly:

    (m+1) + (n+1)
    = 2 + (m+n)         definition of +
    = 2 + (n+m)         inductive hypothesis
    = (n+1) + (m+1)     definition of +

Formalizing this approach first requires generalizing rec-Nat-Nat to ind-Nat-Nat, and giving a simple formal proof of comm-plus.

Problem 5. Prove that plus and + are the same function, and use this to infer that the usual addition is commutative via comm-plus.

Problem 6. Formulate another theorem, along the lines of max-monus-theorem of Problem 3, but relating min, max, and diff, and use ind-Nat-Nat to prove it.

Pie Repo

I've set up a repo for Pie code that I'm working on. The repo currently contains two files: TreeLib.pie (yesterday's code), and max.pie (which includes implementations of the max and monus function, along with supporting proof objects). The code in max.pie is obviously begging to be re-written as a single general function, along with the corresponding proof objects, which are then used to implement the rest.

Assuming you have an .ssh key registered with mit.cs.uchicago.edu, you can clone my repo via

    git clone git@mit.cs.uchicago.edu:saks/pie.git

11/27/18

I'd like to introduce the "Tree problem" for Pie. Is it possible to implement a reasonable tree data type in Pie? I'll go through some ideas and bottlenecks.

11//6/18 — Election Day

Today we read through Chapter 13 of “The Little Typer,” we will finish the book next time.

10/30/18

Today we reviewed some of the equality eliminators of Pie, including cong, replace, symm, and trans, and gave implementations of cong, symm, and trans in terms of replace. We considered briefly the ind-= eliminator, which appears to offer additional power over replace, although we're currently at a bit of a loss as to how to use it.

Please read through Chapter 13 for next time.