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.

Racket 7.1

Version 7.1 of the Racket language system is out. Pie seems (based on unscientific impressions) to be much faster under 7.1 than it was under 7.0.

10/23/18

No meeting! Keep working!

10/16/18

We worked through the proof double=twice, discovering how Pie handles equality as a type, including the use of cong, and trans.

Note that there will be no meeting on 10/23 (Prof. Kurtz has a College Council meeting), and so our next scheduled meeting is for 10/30.

For next time, read through Chapter 10.

10/9/18

We worked through a variety of functional programs in Pie, including a correct version of the concat program. Along the way, we discussed Π-types, and about how -> is a special case of Π.

For next time, read through the Recess following Chapter 7 of “The Little Typer.”

The Deep State Mailing List

I've had an email list set up for our conspiracy. To join, just go to deep-state, provide your credentials, and you're good to go.

Our First Meeting

At our first meeting, we

• agreed to read “The Little Typer” through Chapter 4 (but read below), and
• seriously outgrew our space, with twenty participants in a conference room intended for eight.

We'll be moving to JCL 298.

Now that RSS readers are no longer really a thing, we should set up an email list to augment the blog.

I'd also like to suggest a slight extension to our agreement, as I believe it's realistic to work through Chapter 5, and that by doing so, we can possibly hold the “Little Typer” part of our conspiracy to three weeks.

As a final note, I observed during the seminar that the implementation of concat in the book is bogus, as it reverses its second argument. This raises the interesting problem of giving a correct implementation for concat, i.e., a version of append that relies on recursion on its second argument, and uses snoc to post-pend an element to a list. Please try. I have one, and would like to compare solutions next time.

Getting Started

Our first public meeting will be on Tuesday, October 2nd. I'd like to begin by working through “The Little Typer,” by Daniel P. Friedman and David Thrane Christiansen.

Welcome

Welcome to the Deep State Conspiracy!

We meet at 3:00pm-4:30pm on Tuesday's in JCL 280 for a discussion and/or presentation related to logic or type-theory in the context of computation.