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.