Re: integer exponentiation with negative exponent

[Coda Highland <chighland@...>]

On Sat, May 17, 2014 at 2:13 AM, Thomas Jericke <tjericke@indel.ch> wrote:
> On 05/17/2014 04:36 AM, Coda Highland wrote:
>>>>
>>>> As soon as any static analizer hits a function call, it wont be able to
>>>> decide this anyway.
>>
>> That's not true, a sufficiently complex static analyzer can define
>> inference rules for the return type of a function in terms of its
>> parameters.
>>
>> I spent a lot of time bashing ACL2 into listening to me. :P
>>
>> /s/ Adam
>>
> This is just possible for some Lua code, not for all, look at this:
>
> local int = true
> function test ()
>     int = not int
>     if int then
>       return 1
>     else
>       return 1.0
>     end
> end
>
> while true do
>   print(test())
>   yield()
> end

Well, sure, it's possible to write functions that can't be reasoned
about. The halting problem proves this is so. But function calls
aren't fatal issues in and of themselves -- but the static analyzer
should be able to determine that it KNOWS it can't reason about
test().

Or if it's particularly sophisticated it can admit test()'s return
type as "number" or as "int|float" instead of "int" or "float". It's
still possible to reason on this signature, since you can at least
recognize what operations are legal on it.

If it's EXCEPTIONALLY sophisticated it can recognize that test() has
bound an upvalue and consider the upvalue to be part of the function
signature. It can admit a return value of something like "'int' ? int
: float". We're hitting diminishing returns at this point, especially
since such reasoning can't be done about C functions (at least, not
without manual annotation), but it's still possible to reason about it
in this case.

(My honors thesis project in college was, before circumstances forced
me to drop it, going to concern provable software, hence why I spent a
lot of time in ACL2.)

/s/ Adam