Skip to main content

Cut Elimination

I was thinking about cut elimination on my way back from work today due in large part to a post on the cut rule made by sigfpe on A Neighborhood of Infinity.

It occured to me that the fact that cut-free proofs can be so tremendously much larger than the cut-full ones and that directly constructing cut-full proofs is so difficult is a bit strange. It seems somehow unfair.

As I was thinking about this I realised that one could find cut-free proofs automatically and then reduce them with reverse cut-elimination to produce extremely cutfull proofs. These proofs should be very economical computationally. If one keeps the terms that correspond with the proofs along side, one should be able to obtain a source to source translation that might have performance benefits.

Another totally far-out idea came to me as well. Mathematicians often use lemmas repeatedly. Perhaps the process of finding cuts is generally useful. Specifically, if a lemma is useful in simplifying one proof, maybe it is more likely to be useful in simplifying other proofs. There should be statistical measures over random syntactically valid sentences that one could come up with to see if such lemmas exist.

Comments

Popular posts from this blog

Decidable Equality in Agda

So I've been playing with typing various things in System-F which previously I had left with auxiliary well-formedness conditions. This includes substitutions and contexts, both of which are interesting to have well typed versions of. Since I've been learning Agda, it seemed sensible to carry out this work in that language, as there is nothing like a problem to help you learn a language. In the course of proving properties, I ran into the age old problem of showing that equivalence is decidable between two objects. In this particular case, I need to be able to show the decidability of equality over types in System F in order to have formation rules for variable contexts. We'd like a context Γ to have (x:A) only if (x:B) does not occur in Γ when (A ≠ B). For us to have statements about whether two types are equal or not, we're going to need to be able to decide if that's true using a terminating procedure. And so we arrive at our story. In Coq, equality is ...

Total Functional Programming

Recently on Lambda the Ultimate there was a post called "Total Functional Programming".  The title didn't catch my eye particularly, but I tend to read the abstract of any paper that is posted there that doesn't sound terribly boring.  I've found that this is a fairly good strategy since I tend to get very few false positives this way and I'm too busy for false negatives. The paper touches directly and indirectly on subjects I've posted about here before.  The idea is basically to eschew the current dogma that programming languages should be Turing-complete, and run with the alternative to the end of supplying "Total Functional Programming" .  At first glance this might seem to be a paper aimed at "hair-shirt" wearing functional programming weenies.  My reading was somewhat different. Most hobbiest mathematicians have some passing familiarity with "Turing's Halting Problem" and the related "Goedel's Inco...

Type Checking and Cyclic Proof

Standard functional programming languages like Haskell and SML use polymorphic type systems. These type systems however, are not sound. What this means is that the type-systems themselves can not be used to prove properties of the software in the sense of "total correctness". To see that this is true, we can get a "proof" (read program) of inhabitation of any arbitrary type A, by simply using the program: data Bot {- Look Ma! No constructors! -} bot :: Bot bot = bot Clearly when we say that bot is an inhabitant of Bot, we dont mean that it actually produces a value of type Bot, since there aren't any as Bot has no constructors! We can easily use this type of proof to prove something like A ∧ ¬ A which leads to a pretty degenerate logic. However, the type system is still *useful* in the sense that if the program ever *does* terminate, it's sure to do so with the appropriate type. This means we can get the full class of Turing complete programs, a...