|
[May. 30th, 2005|07:05 pm]
Jason
|
I got in full-bore obsessed-with-math-problem-mode today. It was pretty fun, although after about six or seven hours of it I'm tired but not done with the problem. Somewhat frustrating.
The punchline is that I think I've found an interesting new type system which is a generalization of Pure Type Systems to handle a very large family of occurrence-based substructural features, including but not limited to linear, affine, and relevant (AKA strict) lambdas and pis, at every sort. The difficulty is, strangely enough, that I'm having trouble working out what exactly the weakening lemma needs to be, something that is ordinarily very easy, but since reexamining the status of variables in the context is kind of central to the endeavour, I guess I shouldn't be too surprised. What's very nice is that it seems I'm able to say, "okay, suppose there is some finite set of 'modes' for variables (e.g. 'linear', 'unrestricted') with some operations plus, times and a relation less-than defined on them" and I can blast ahead trying to prove the substitution theorem and the proof attempt basically tells me what algebraic laws need to be satisfied. The fact that substitutions need to commute with each other requires associativity of multiplication, the fact that substitution commutes with application needs that multiplication distributes over addition, etc. It'll be very cute if it all works out. |
|
