Lambda the Ultimate

Hi,

The idea is not to compute the ranges given a formula in ordinary logic. But to have a logic that allows to express the ranges in its own language, including a semantics, substitution rule, etc.. for this new logic. Computing the ranges is easy, I have already given an algorithm in my question itself. Namely right associative mini-scope gives start and left associative mini-scope gives end.

This logic would for example allow manipulations such as renaming a variable range. Thus effectively saving one variable name. This is not possible in normal logic as one can easily figure out, i.e. p(X), q(X,Y), q(Y) is not the same as p(X), q(X,X), q(X). But why not use X inplace of Y, after X is anyway not used anymore.

I am interested into whether somebody has already come up with a corresponding calculus. The calculus would govern the manipulations, so that movements that would change the meaning, like for example by variable clashes, are not possible.

Best Regards

Hi,

Thank you very much for your comment and the very interesting
links. The difficulty I am facing is that I have only this
graphical idea in mind and don't know yet much about the
possible rules that would govern the concept.

Concerning some doubts whether graphical ideas can be formulized.
I think knuth was facing the same problem when he created TeX.
And I guess the resolution was that a linearisation even of
2-dimensional concepts is most often easily possible.

But compared to TeX the 2-dimensions here are not boxes and
their juxtaposition or inclusion, but rather something that
reminds me of proof nets in linear logic. If we could model
variable start and end as positive and negative literals we
would eventually be done.

I forgot to post the motivation behind this kind of logic.
My primary motivation is currently some code generation.
But today I came up with some additional possible
application areas. So my list now goes:

- Compiler Backends: Register Allocation
- Code Verification: Proof Statements
- Natural Language Processing: Anaphora
- Database Systems: Query Optimization
- Logic Programming: Partial Evaluation
- What else?

I have already looked a little bit into the register allocation
literature. There are some results, like from Chaitin, that
register allocation corresponds to graph coloring. Also if I
look at the papers I see that the authors have a refined
language to talk about the issues: live interval,
use position, etc..

When looking at the domain of register allocation, then one
might ask oneself how this domain, a sequence of expression
assignments, eventually if-then-else and while, are modelled
in a functional programming language. I guess monads are
here in use. I have even seen monads covering non-determinism.

But what I have not yet seen, these monads interspersed with
quantifiers, as the graphical intuition would suggest. Maybe
a quantifier corresponds to a variable declaration block. But
then we end up with hierarchical variable scopes again, and
not the overlapping thing I have in mind.

So if somebody has already put hands here, I would be very
interested to know about.

The problem with scope extrusion would be possibly that
the number of needed variable names increases. Something
which is counter to the intended application areas.

So if you have graphically, in this not yet fully
identified logic:

           +--- Y ---+
   +--- X ---+    +---- X ---+

Then when we translate it into normal logic via scope
extrusion, we can only arrive at:

   +----------- Y -----------+
   +----------- X' ----------+
   +----------- X -----------+

We have to rename one of the X, because the quantifier
extrusion rule has a side condition:

      exists X(A & B) = A & exists X B     if    X not in A

Right?

Although my question could give the impression
that I am interested in scope extrusion, I guess
scope extrusion will be not a dominant rule of
this not yet fully identified logic. Since the
logic should be able to deal with variable occurence
ranges, the contrary is the case. The interest could
be more characterized as "scope intrusion".

By these ranges, a new, more intrusive, way of
defining a scope should be possible. The quantifers
should be able to intrude into the conjunction
boundaries independently of each other.

Best Regards

Thank you very much. This could work. Would need to look into it in more detail. I guess the non-linearity is not a no-go. Since the linear case, as you showed, is simply a special case.

Little excursion: Interestingly removal of assumptions is even a sound rule, also in normal sequent logic. If we look at the assumption introduction rule, which would read (the rule is named according to forward chaining, but removal amounts to introduction in backward chaining and vice versa):

   G, A |- B
   ----------- (Right Implication Introduction and Assumption Removal)
   G |- A -> B

One could also define the following rule, which is more or less the inverse of the previous rule. It would not define a complete fusion operator & though. The rule reads:

   G |- B
   ------------- (Right Fusion and Assumption Introduction)
   G, A |- A & B

Its just a short-hand for the valid:

   ------ (Id)
   A |- A     G |- B     
   ----------------- (Right Fusion Introduction and Assumption Fusion)
     G, A |- A & B

Very currious now to look into your proposal.

Just noticed that the "unlet" could also be a solution to a question I already have for a long time. A consume/produce modal operator in logic. It conflicts a little bit with the way linear logic does deal with reasources. Since it would give control of the resource consumption to the query and not to the premisses.

For more detail see here:
http://mathoverflow.net/questions/78557/can-consume-produce-be-modeled-in-linear-logic

I expect that q(X,Y) & q(X,Y) can be simplified to q(X,Y) isn't it?

I was just trying to rewrite your formula in a way which matches better the graphics - and which keeps X and Y separate. Redundancy, yes maybe.