i'm revisiting these ideas because i would like to flesh out the story of logic as distributive law. In a nutshell the core idea in the indexed composition proposal comes out of the fact that we can model a term language as an algebra (read monad), T, and a collection as a monad, S. Then formulae are interpreted as building terms over collections. The completeness of the logic is witnessed via a distributive law, l : ST -> TS. That is, every collection of terms can be written as a term of collections. This is a nice framework for the semantics of formulae, but what about proofs?

The thought i've been following is that indexed compositions are the key form of witness to internalize proof. Valid formulae have a normal form as an indexed composition. In some sense that's another way to look at the content of the algebraic databases post. Consider a basic form

f = { (a,b) | a <- A, b <- B, c

_{1}(a,b),...,c

_{n}(a,b) }

and another form

arg = { a | a <- A, c

_{1}'(a),...,c

_{m}'(a) }

We can construct

{ b' | (a',b') <- f, a' <- arg, c

_{1}''(a',b'),...,c

_{k}''(a',b') }

More suggestively, we have something of the form

f = { (a,b) | a <- A, b <- B, c

_{1}(a,b),...,c

_{n}(a,b) },

arg = { a | a <- A, c

_{1}'(a),...,c

_{m}'(a) },

c

_{1}''(a',b'),...,c

_{k}''(a',b') in Admissible

------------------------------------------------------

{ b' | (a',b') <- f, a' <- arg, c

_{1}''(a',b'),...,c

_{k}''(a',b') }

This looks and feels like a cut rule. It also looks and feels like a join. Moreover, there's a procedural way to get this construction from the logic-as-distributive-law. There are some subtleties, however. For example, there are lots of ways to cut two structures together that still conform to this general scheme. Are there conditions that ensure cut elimination?

## No comments:

Post a Comment