larrλtheliquid -> Lemma the Ultimate

Progress Report & LCHI

2009-11-02T00:00:00-08:00

Progress Report & LCHI

Recap

After having gotten through chapters 0-3 of the Agda Course, my original plan was to keep charging through chapters 4-6. However, during the process of writing an intro to proofs-as-programs I began to notice something that bothered me. In various pieces of literature covering this domain, the notions of axioms, postulates, and judgments are used with different meanings and not clearly elaborated. Additionally, precisely defining how the previous terms and implication relate to one another is tricky. I wanted to write a post that clearly explained how these things related to one another, but I did not have enough background knowledge to do so. One quality of this field is that things are usually precisely defined, so getting away with wishy-washy explanations or guesses doesn’t work =)

Exploring Fundamentals

Rather than continuing with the Agda course, I have begun to brush up on fundamentals by reading through LCHI. Even though each chapter is only 20 pages, the book is packed densely with information and references a lot of discrete topics that I’ve had to refresh my memory of (and sometimes learn).. so it’s a slow but enlightening read. I’ve finished the first chapter, which explains the untyped lambda calculus, but does so formally in terms of what the book calls pre-terms. The purpose of this is to define lambda terms as alpha-conversion equivalence classes of pre-terms, avoiding the handwavy notion of just identifying alpha-equivalent terms. It’s a pretty neat formulation, and other equivalence relations like beta and eta are defined on these lambda-term sets.

Next Up

I’m in the middle of chapter 2 right now, which is on intuitionistic logic. My plan is to finish this chapter as well as chapters 3 and 4 on the simply typed lambda-calculus and the Curry-Howard Isomorphism respectively. As I’m reading this I’m taking notes that will be used for a post that clarifies the relationship between axioms, judgments, and implication that I mentioned earlier. In particular, chapter 2’s natural deduction explanation as a formal version of the BHK intepretation of logical connectives in intuitionistic logic includes a simple definition of implication in terms of judgments (in the introduction and elimination rules). With chapters 1-4 done I think I’ll be able to write the aforementioned post and be able to sleep soundly about the explanation. Once again, although I’m already familiar with the topics covered, the level of precision used in LCHI makes it a slow but gratifying read… highly recommended if you have the will-power =)

Intro to Proofs-as-Programs

2009-10-24T00:00:00-07:00

Intro to Proofs-as-Programs

Foreword

This post is meant as a very basic introduction to the notion of Proofs-as-Programs. Like many fields, herein lie simple concepts that are obscured by notation and vocabulary, so I try to point out synonyms where possible to avoid future confusion. Agda is used to explain these concepts as realized in an actual programming language.

Proofs-as-Programs

Proofs are a formal topic requiring a lot of background knowledge and experience in math and logic. Due to this, many programmers get turned off when the word proof is uttered. As it turns out, an elegant analogy exists called the Curry-Howard Isomorphism. The basic idea is that values are to types as proofs are to formulae. With this stunningly simple correspondence, it is possible to reuse years of programmer experience in typed languages and get those programmers on the path to theorem proving. What follows explains a different way to think about programming, from the eyes of a theorem prover. However, take notice that only basic standard programming concepts are utilized!

Getting Started

Programming is done in a logical system, therefore almost no functions or types exist at the onset. Proofs rely on incrementally building up knowledge from previous knowledge, therefore we must define all types and functions used ourselves in the language we are using (of course, source code for common types and functions can come as part of the language in its standard library). The canonical domain we will be using is that of natural numbers (integers from zero to infinity).

Defining Types

data Nat : Set where

We start with the code above by creating a new type called Nat representing the type of natural numbers. Nat is assigned a new unique value of type Set. If you think about it, a type is a set whose elements are values of said type. Because of this, Agda uses Set as the base type from which other types are born.

Defining Values For Types

data Nat : Set where
  zero : Nat

Just as we created a new value of Set called Nat, we now create a new value of Nat called zero. In other words, zero is a value whose type is Nat. For all intents and purposes, you can think of this zero as an atom in other programming languages. For now we will use this partial definition of the natural numbers set, consisting only of zero.

Value Judgments

A judgment/assertion is a value/type pair, which asserts that the value is of its pairs type. It is the compiler’s job to check if the value/type assertion is correct. If we adopt the mindset of proofs-as-programs, then a type is some formula that we wish to derive with some proof in the form of a value.

natsExist : Nat
natsExist = {!!}

Here we would like to prove the existence of natural numbers. We represent this as a variable with a type of Nat that we must assign to some unknown. In other words, the goal is to prove the existence of Nat by assigning a value that matches the type of Nat. Agda uses {!!} as notation for a thus far unproven goal that you may use a placeholder when constructing your proofs.

natsExist : Nat
natsExist = zero

With the completion of our goal, we now have a judgment. In order to see if a proof “checks”, the compiler makes use of what are called inference rules. An inference rule can have 0 or more premises/pre-conditions that must be met to imply/prove/derive some conclusion. In our case the zero : Nat judgment is derived by the zero : Nat data type that we defined earlier, which acts as an inference rule with 0 premises. When this happens the compiler determines that our proof “checked” and natsExist is assigned to a trusted proof of Nat. In effect, it has itself become a new inference rule.

Teatime

Take a moment to pause and reflect on the fact that we are merely discussing simple static type checking. Nevertheless, thinking of these things from the point of view of a theorem prover is a fun and enlightening exercise. However, this isn’t just fun and games, as the simple analogy will let you make powerful claims once you learn more. Another insight to ponder is that the relationship between proofs and formulae is many-to-one. This is an important observation because it means that there are many ways to prove the same thing, making your chances of finding just 1 proof (that’s all you need) greater.

Function Judgments

Proving a value judgment was pretty easy, so let’s try proving a function judgment. For this we will attempt to create a judgment add representing the addition of 2 natural numbers.

add : Nat -> Nat -> Nat
add = {!!}

As before, we start off with a type declaration and a goal. The type of add indicates that it is a function which accepts a Nat, which returns a function that again accepts a Nat, which finally returns another Nat. Before we go on, realize that the ultimate intent of this judgment is to prove the existence of Nat (the same goal as the previous value judgment!)

add : Nat -> Nat -> Nat
add = \(x : Nat) -> {!!}

After compiling, we are assured that the first premise has been proved via an anonymous function that accepts a Nat as an argument. In order for this typed lambda judgment to be proved by the compiler, several built-in inference rules are used that correspond to the typed lambda calculus (although it’s not necessary to understand these in detail, as the rules are intuitive… no pun intended =).

add : Nat -> Nat -> Nat
add = \(x : Nat) -> \(y : Nat) -> {!!}

Once again, the second typed lambda judgment we presented is verified by the compiler. Take a second to think about what this function has verified so far. One may jump to a conclusion and think that we already proved Nat in the first argument, so why even prove it in the second argument and result? However, even at this step we haven’t proved Nat. Arguments in functions correspond to premises in induction rules (see the next paragraph).

add : Nat -> Nat -> Nat
add = \(x : Nat) -> \(y : Nat) -> natsExist

Here we finally prove the conclusion (the return value), and we get to do it with the natsExist proof we wrote earlier (zero would have worked just as well)! But, realize that what we’ve really done is created a new inference rule with 2 premises. Therefore, our proof of the conclusion is not valid unless 2 proofs for each premise are supplied. In this simplistic case all 3 judgments prove the same formula. Thus getting access to the return value proof is not particularly appealing as you already have at least 1 proof of the same formula supplied as the first argument of the function (recount that proofs to formulae are many-to-one).

A Step Back

The power of proofs-as-programs is that you can encode more powerful constraints of functions and values into their types. The canonical example is (using dependent types, a subject of a future post) a sorted list insertion function that guarantees that the returned list remains sorted (along with other properties you may want to ensure such as the size being preserved, elements being preserved, etc). That said, addition is simple enough that we merely want to use its return value for computation rather than for a proof of Nat. The good thing is that you can decide where the boundaries lie between simple functions and types, and complicated functions that require type-based constraints (e.g. remaining DRY through the use of various complex combinators, but ensuring the function does what you want in its type.

Completing Nat

So far we’ve worked with Nat as an incomplete set (it only contains zero), so let’s fill the rest in.

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

The rest of Nat is achieved via an inductive type definition, yielding an inductive type. The similarity to mathematical induction should make sense to anyone with a CS background, but basically you can think of it like a recursive definition. So, succ accepts another Nat which may be zero or another nested succ, e.g. succ (succ (succ zero)) representing the natural number 3. The addition function we defined earlier still works because we chose a general type, but let’s make it return what we intended. Before we do that, we will first rewrite the function to use a syntax sugared version that performs pattern matching on the lambda arguments.

add : Nat -> Nat -> Nat
add x y = natsExist

Coverage Checking

add : Nat -> Nat -> Nat
add x zero = {!!}

If you attempt to compile the above you get an error, but why? When we defined Nat with the data directive, we once and for all defined all possible values. Agda requires functions to be coverage complete with respect to type values! Now that we switched to pattern matching on the specific value zero, Nat coverage checking fails and the compiler tells us to also define the function for the succ case.

add : Nat -> Nat -> Nat
add x zero = {!!}
add x (succ y) = {!!}

With coverage checking you are not only assured of compile-time type safety (only Nats), but also that functions are defined for all possible values of a type (you can still encode type-level restrictions as long as all cases are accounted for, but that is again a subject of another post).

Completing add

The actual function implementation isn’t the purpose of the post, so I’ll quickly list it here.

add : Nat -> Nat -> Nat
add x zero = x
add x (succ y) = succ (add x y)

Axioms

You may have noticed something fishy about the data type definitions. In particular, the definition for zero is similar to natsExist, but there is one key difference. Namely, zero does not provide a proof/value of its formula/type. Defining something this way creates an axiom/postulate. Using data actually creates a restricted postulate that does not allow types like Nat to have additional values defined in them later (if this were allowed, any coverage-based reasoning would no longer be true). Additionally, the property of coverage is enforced in future functions (with respect to the values of the newly defined type) when you use data.

Q.E.D.

I hope you enjoyed this post, as that’s it for now. Once again, the example code produced is trivial but necessarily so to explain the concepts. Proofs-as-programs starts to be a very powerful concept with the introduction of Dependent types… be patient as that post will come later =)

Bonus: Syntax Sugar

Agda also let’s us write prettier code with unicode and mixfix operators. I left this out until now to avoid cluttering the explanation of more important concepts.

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
x + zero = x
x + succ y = succ (x + y)

succ2 : ℕ → ℕ
succ2 = λ x → x + (succ (succ zero))

AgdaSpec Hackery

2009-10-23T00:00:00-07:00

AgdaSpec Hackery

AgdaSpec Examples

I played around with the idea of writing a friendly RSpec-like dsl for Agda. You can see the result below. It was just some late-night experimentation and I have been concentrating more on catching up on Lambda-Calculus, logic, and theorem proving fundamentals, so consider it less than a proof-of-concept for now. That said, I plan to come back to the idea of a more friendly dsl for Curry-Howard testing including universals once I'm more experienced.

module UsingAgdaSpec where
open import AgdaSpec

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

-- Equal terms compile
postulate zeroEqualsZero : specify zero and zero are equal
postulate oneEqualsOne : specify (succ zero) and (succ zero) are equal

-- Unequal terms raise compilation errors  (uncomment line below to see said errors shown in the comments for convenience)
-- postulate zeroEqualsOne : specify zero and (succ zero) are equal

-- zero != succ zero of type Nat
-- when checking that the expression equal has type
-- Expectation zero → Expectation (succ zero)

Implementation

The nice thing about the code above is that equals is merely a function that conforms to the type signature of a binary relation (in other words, a single argument function). That means you can define arbitary functions easily to extend the "library" with other custom "matchers". The "specs" are run at compile time, which means you don't get code back unless your tests pass. Additionally, tests will return proofs of their type-based specifications, which means you could reuse them compositionally to produce more complex tests/specs. Finally, the dsl'ish trick is accomplished by using a mixfix function definition in Agda via underscores in the name.

module AgdaSpec where

equal : {Poly : Set} -> Poly -> Poly
equal identity = identity

data Expectation : {Poly : Set} -> Poly -> Set where
data specify_and_are_
{Poly : Set}(a : Poly)(b : Poly)
(c : Expectation a -> Expectation b) : Set where

Agda course update

2009-10-18T00:00:00-07:00

Agda course update

Status quo

I just finished chapter 3 and am starting on chapter 4 in the Agda course. Chapters 0 & 1 starts off nice and light, giving an introduction to the course. One very nice feature of chapter 1 is a gradually built up explanation of dependent types in context of more familiar monomorphic and polymorphic static typing in languages like Java, C++, and Haskell. Chapter 2 changed abruptly to explaining what reduction systems are, but don’t be deterred! Although the relation to dependent types is not clear in chapter 2, chapter 3 explains the untyped and simply typed lambda calculi. In these chapters you’ll see that a given lambda calculus can be modeled as a reduction system where T is the set of lambda terms, and beta-reduction (along with alpha-conversions) constitutes the binary relation. Although a lot of complex sounding words are used (beta-redex, beta-reduct, etc.), the underlying concepts are not that complicated. More importantly, chapter 3 ends in explaining the Curry-Howard isomorphism and what it looks like in Agda. At this point I prefer Agda’s approach of a unified system using types for everything, compared to Guru’s split between terms/types and proofs/formulae with respect to operators and syntax. Note that after finishing chapter 3 you should be able to to watch the University of Oregon Logic and Theorem Proving summer school intro video and be comfortable with all the material.

Next up

I’m going to continue reading the remainder of the course slides. Between what I’m learning in this course and what I’ve learned from the Guru book I think I’ll be able to write a good intro to dependent types post for those that do not wish to read the more theoretical material. More importantly, I have an incomplete draft post that I’m very excited about. The purpose of the post is to explain what dependent typing (and theorem proving therein) is in the context of dynamic typing, static typing, Test-driven development, and program verification in general. I’ll probably wait until I’m finished with the Agda course publishing these two. The second post especially could be an understandable and sensible reference to give to industry programmers so I’d like to get the argument right. That’s all for now, see you again soon!

Roadmap

2009-10-14T00:00:00-07:00

Roadmap

Status Quo

After having completed the Guru book I did a brief and shallow survey of the field to see what to learn next. To skip to the chase, I will currently focus on learning Agda next. If you are interested in why, then continue reading as I briefly discuss some alternatives that I did not choose for now. Please be aware that my experience with the following is slim to none so my opinions could change drastically in the future. The plan is to invest in learning Agda now, then come back to read more general Curry-Howard and proofs-as-programs books later while transcribing examples to Agda for greater understanding. I have also spent a bit of time working on a toy implementation of the declarative Oz kernel language for elementary experience in language construction in case I feel an itch to move in that direction. I will come back to this from time to time for a small change of pace.

Agda

What’s nice about Agda is that it feels like a very natural extension of Haskell. Haskell got a lot of things right in the way of mutation-restriction via monads and powerful type inferencing. Although it recently added Generalised Algebraic Data Types they are still not as flexible as completely dependent types. Agda on the other hand fills this role quite well, in fact it is itself implemented in Haskell and even makes code sharing possible. To be fair, most proof-based languages are implemented in an ML dialect or Haskell, in contrast to the C/C++/Java dna of more traditional languages. I like Agda right now for two reasons: First it has a strong emphasis of purely functional code which is much more pleasant to deal for learning. And secondly it deals with manipulating raw proofs directly rather than using “script” abstractions. It may turn out that both of these advantages disappear after I get passed the learning stages of this field, but from briefly looking over the language it seems cohesive enough to still be practical even after learning… And a third more selfish reason is that Agda comes with a very fun Emacs mode =) My first focus will be going through this Agda course available online.

Coq

Coq is one of the older (but still actively developed) and more mature proof languages / systems. There is a well-organized Software Foundations course based on Coq available, as well as an ICFP video explaining its background… these are both by Benjamin Pierce of TAPL fame. Unlike Agda, in Coq one uses tactics to write “proof scripts” for proving. These are a higher-level abstraction than bare-bones equational reasoning. Although this sounds great in principle, like I already said I’d rather dabble at a lower level right now because I think it may result in a better base for learning. Coq also has much more literature in doing imperative proofs that I’d like to steer clear from. Either way, once I have a better foundation with Agda I will definitely revisit the course linked above to mirror exercises in it. Coq is one of those widespread languages that you cannot afford to not learn. Well… at least widespread in this community =)

Epigram

I have not dug much into this language. However I do know that is also written in and similar to Haskell, and the most comparable to Agda. A new significantly improved version of Epigram is in the works, which can be tracked at this developer blog. In fact, all of the languages in this post are still in very active development, for example check out the notes for the recent Agda developers annual meeting.

Twelf

Curry-Howard, Martin-Löf, and the calculus of constructions are all very cool ways of brilliantly relating standard programming to proofs. That being said, Twelf uses LF to take things one step further. Syntax comes as a third player to the field, making for a very unifying and grand theory. Yes… even something as unassuming as syntax stands on level ground with standard programming and proofs via things like Higher-Order Abstract Syntax… therein you can call syntax as if it were a function to perform variable substitution and eliminate a large class of variable capture problems… amazing!!! You can find a great video and mini-course about Twelf… it was part of a recently held summer school made available for free including course materials and videos (many other similar topics are covered, of course including Coq). The Twelf lectures are presented by Robert Harper of CMU so hold on to the railings for an exciting roller-coaster ride. Dr. Harper is also offering what looks like a great programming languages (in-progress) book draft for free. I will come back to Twelf later with the most excitement, mainly due to the fact that its intent is to focus on proving about formal properties of languages rather than integrated proofs for general-purpose programming. I haven’t dug in enough to know if this is just what Twelf has been used for historically or if there is some limitation. Another reason for saving this for later is that I need enough mental energy to focus on just learning on an isomorphism =p

Conclusion

So there’s my roadmap, full of fun links and hopefully a reasonable approach to diving into the exciting field of theorem proving. To summarize, the plan is to first learn Agda and then move on to more theoretical books, and finally come back to go through Coq and Twelf courses to compare each additional language I acquire knowledge about with the previous ones. Although I wasn’t expecting it, there is plenty of approachable information available. That means there are no excuses to not to explore this stuff, so join me if you would like =) As always, during the course of my learning I may find reasons to change the order I outlined above, so no promises about that. I should also note that I may dabble with going through and reworking some of the Real World Haskell book as I am learning Agda. Finally, please be kind and leave any good resources you may know of in the comments.

Hello world!

2009-10-13T00:00:00-07:00

Hello world!

Introduction

This is the first post of what I hope will be many small but frequently posted reflections. Reflections on what exactly? Trying to find ideal methods to build software (see the first paragraph on the homepage for details). In posts such as this one I will give updates on things I learn as I encounter them. In the sidebar on the homepage I will update my opinion of what I guess to be most ideal languages for writing reliable software, my current hypothesis of what reliable software entails, and whatever current project I am doing research on in an attempt to formulate more reliable guesses of the previous two things.

Why

Most of my programming experience has been with Ruby and various other dynamic languages including Common Lisp, Oz, & Clojure. While I enjoy using these languages, their losely restricted mutability (especially in Ruby & CL, but even in Oz & Clojure) gradually leads to time spent in the debugger, inspecting the state of things before and after each line to figure out why something strange is happening. Dynamic typing had its golden age, but with sophisticated type inferencers (most notably like what Haskell offers) the pain of types is drastically reduced to a prick of the finger. More importantly, those types become practically necessary to do any sort of universal quantification based reasoning on code. Such reasoning allows for proofs that can state properties about all instances of certain types of functions, even polymorphic types!

How

Although the exact details of how to achieve this "verified", or reliable, style of programming is the topic of this blog, I have two important points to wage bets on already. Proofs about universals ("for-all" statements about some properties such as variables or function arguments) eliminate a lot of instances of those aforementioned debugger sessions. An important mindset that I've aquired in my career is that of Test-driven Development (TDD). Programs, through use of composition to manage complexity, still remain complex enough to require extra code to make sure that the compositions actually accomplished the original intent (i.e. tests). The epiphany is that tests (assertions) are merely the simplest type of proof (join proofs, or proofs by interpretation). Many other types of proofs exist (contrapositive, inductive, equational, etc), but there is another reason besides universals to use proofs. When typically writing a new test, or an entire suite, you start from scratch everytime. This contrasts starkly with the way other code is written. More specifically, regular code is written compositionally by building up libraries (even frameworks) of abstractions to make it easier to manage. There aren't many effective ways to compositionally build up tests. Even if you try, in dynamic and unrestrictive-mutation based languages the tests usually rely on setup/teardown that becomes too difficult to reason about sanely. On the contrary, a proof (the code that proves an expected theorem under the Curry-Howard isomorphism) can be reused to build another more complicated proof! A formula can be viewed as the type of a proof that tries to prove it.

Curry-Howard

Under this isomorphism, a type is a "kind" of some value expression. The complement to this relation is that a formula is a kind of some proof. Take a moment to contemplate this, it has profound implications... Notice that the relationship between proofs and formulas is many-to-one. There can be several ways to prove something but only one formula that it proves. What happens in our model when a proof does not succeed in proving some formula?... a typing error caught by compilation! Proofs (and in certain languages even types and formulas) become values themselves, leading to the composition property in testing... and also the pun on the "lambda the ultimate" title of this blog... Just imagine for a second "calling" a universal proof with a value of a specific instance that you would like to prove... this is possible and even normal under this isomorpishm... the whole idea, like many things, is old but unappreciated and heavenly.

Guru

Guru is a language currently being developed and preparing for 1.0. If you are unfamiliar with what I'm talking about, please take the time to read the book found in the doc directory of the language. Solutions to the exercises (which I recommend doing) are also found there (see my similar solutions if you would like). I warn you that the language does not attempt even modest type inferencing. Its concept of using resources to model declarative code efficiently with imperative code in my opinion becomes impractical to deal with. This is made obvious by the definition of the non-trivial map function for which the author teaches with a simple example that is a stark contrast to the version included in the distribution. This problem is exacerbated by the language's reliance on partial evaluation in proving, for which you need to look at previous function and type definitions. Nonetheless, the language is generally fairly simple and the book is an amazingly simple introduction to this type of programming.

Concurrency

For the time being, while I am learning I will be ignoring concurrency even though it is already a modern problem. I think dataflow concurrency could be a natural and easy thing to exploit in this declarative world, although I am not sure (although dataflow remains declarative it is potentially non-terminating, and non-total functions are a pain to prove anything about... relating to the Halting Problem). In general declarative programs are easier to prove things about though, so hopefully I can come back to this topic later without too much pain.

Mutation

You may have noticed that I am trying to find practical ways to build this reliable software but have only alluded to declarative programming. As I am a currently novice in the field of theorem proving, I will only think about the declarative model for a little while. I think languages that restrict mutation like Haskell, and other restriction methods such as Software transactional memory (STM) will make mutation still possible as long as it is thought of as the edge case. Mutation will always be in the back of my mind though, so hopefully I won't stray too far from the path.

Conclusion

That's it for now. I will be posting a lot so check back often or subscribe if this kind of stuff interests you. Tell your friends if you think they would like this, and please leave comments containing helpful links as well as criticisms and other feedback! As a final note I should mention that I have not given up hope on the dynamic languages front... the tone of this blog may indicate that but I am merely playing devil's advocate to explore the other end of the pole.