Lambda the Ultimate

The usual problem with eliminating array bounds checking is that integer arithmetic is undecidable. For example, the compiler can't figure out that you can index into an array of m·n elements using an expression like i·n+j, even if it's known statically that 0≤i<m and 0≤j<n. Or rather, that particular problem is simple, but it's hard to come up with a general algorithm that would work for many different programs. Many people are trying to use dependent types and machine-checkable proofs for that, like in Hongwei Xi's paper.

It just occurred to me that statements like "if i ∈ [0,m-1] and j ∈ [0,n-1], then i·n+j ∈ [0,m·n-1]" (all segments are closed) can be interpreted and proved in real arithmetic, instead of integer arithmetic. The nice thing is that real arithmetic is decidable. If that approach works, we can have a language with integer-parameterized types like "array of n elements" and "integer between m and n", and have a simple definition of what the type checker can and cannot automatically prove about programs using such types, without having to write any proofs explicitly.

Of course the system will be limited by the fact that it's talking about reals rather than integers. For example, there will be problems with integer-specific operations on type parameters, like division and remainder, but I don't know how often these will be required.

Are there any obvious problems with this idea? Has it been tried?

Hi
I tried to make reductions for usual lambda-terms "as for DeBrujn's terms". May be, it will be interesting for somebody
\begin{align*}
&(\lambda xy.x)\,y && \\
&\to [y/x]\circ\lambda y.x && (Beta)\\
&\to \lambda y.\Uparrow\![y/x]_y\circ x && (Lambda)\\
&\to \lambda y.W_y\circ[y/x]\circ x && (LiftShift')\\
&\to \lambda y.W_y\circ y && (Var)\\
&\to \lambda z.\{zy\}\circ W_y\circ y && (\alpha)\\
&\to \lambda z.W_z\circ y && (IdShift)\\
&\to \lambda z.y && (W)
\end{align*}
The line \alpha is "explicit renaming of bound variable". Details are here
http://arxiv.org/abs/1303.5039
The text isn't easy.