FW: Correspondence of Linear Logic & Geometric Algebra

[RE01 Rice Brian T. EM2]

This isn't really something most people would pick up on, but it still
belongs in review, at least for theory and technical terms.

> -----Original Message-----
> From: RE01 Rice Brian T. EM2 
> Sent: Saturday, November 04, 2000 7:39 PM
> To: 'fare@tunes.org'
> Subject: FW: Correspondence of Linear Logic & Geometric Algebra
> 
> 
> I thought this might strike you as interesting in terms of 
> relating various computational views. I am quite busy, but am 
> still developing better documentation, ideas, and specs for 
> slate, tunes, etc. In two weeks I will be back with results. 
> You might forward this to the list if you like.
> 
> > -----Original Message-----
> > From: Tim Sweeney [mailto:tim@epicgames.com]
> > Sent: Friday, October 27, 2000 3:14 AM
> > To: types@cis.upenn.edu
> > Subject: Correspondence of Linear Logic & Geometric Algebra
> > 
> > 
> > [----- The Types Forum, 
> > http://www.cis.upenn.edu/~bcpierce/types -----]
> > 
> > While prototyping a compiler using Girard's Linear Logic as a 
> > type system
> > and implementing, in it, a math library supporting the 
> > Geometric (Clifford)
> > Algebra, I noticed a striking resemblance.  Are these two 
> > systems known to
> > coincide?
> > 
> > My conjecture: Linear Logic and Geometric Algebra are, in an 
> > axiomatic and
> > semantic view, equivalant; as:
> > 
> > - The linear logic's "times" operator corresponds to the 
> > Geometric Algebra
> > outer product.
> > - Linear "with" corresponds to the geometric product, with semantics
> > analogous to the set-theoretic "exclusive or".
> > - "Par" matches the meet operator (the dual of the "times" 
> > and therefore of
> > the outer product).
> > - "Plus" is the dual of the geometric product.
> > - "Nil", A_|_ corresponds to multiplication by the unit 
> pseudoscalar.
> > - The "!" operator in linear logic appear to roughly 
> correspond to the
> > reverse of a multivector, and "?" to the conjugate of a multivector.
> > - The grade of a homogeneous multivector is analogous to 
> the number of
> > linear terms that appear in each conjunctive subterm of an 
> > expression.  GA
> > operations which raise, lower, and retain the grade, are 
> > analogous to linear
> > logic with respect to the number of linear assumptions.
> > - The GA interpretation of linear implication "A -o B" is 
> > (surprisingly) not
> > an exponential, but in fact the inner product, seeing that it is the
> > algebras' sole grade- (uniqueness count-) lowering operation.
> > - The entire duality of linear logic (between conjunction and 
> > disjunction,
> > and so on) is carried out identically to the duality of 
> > Clifford Algebra,
> > between outer products and the meet operation.
> > - The "1", "T", "_|_", and "0" of linear logic correspond to 
> > 1, the unit
> > pseudoscalar, the unit pseudoscalar again, and zero.
> > 
> > Going through Hestenes' book on Geometric Algebra and Girard et al's
> > "Advances in Linear Logic", the correspondence runs so deep 
> > that I find it
> > hard to believe the systems do not correspond.
> > 
> > Interestingly, the development of Geometric Algebra was 
> > developed to treat
> > spaces and their subspaces as first-class constructs in a 
> > single algebra,
> > with the new geometric product bringing together terms of 
> > dimensionality;
> > while Linear Logic was invented to treat uniqueness (in a 
> > certain view, a
> > form of dimensionality) as a first-class construct, using the "with"
> > (do-only-once) operator to formalize the uniqueness dimension 
> > of values.
> > 
> > It would thus be delightful to see that these two operators, 
> > and perhaps the
> > entire formalisms of GA and LL, contain the same substance, 
> developed
> > independently, as they were, almost a hundred years apart.
> > 
> > I would be interested in a counterexample, or references on this
> > correspondence if it is known.
> > 
> > -Tim Sweeney
> > 
>