Comment by dwohnitmok
2 months ago
> That's why you need to modify the type system, obviously. That is not a problem.
What typing judgment rules would you have for RUNTIME?
> On the other hand, if you can prove f x = g x for all x, then you should be able to prove RUNTIME f x = RUNTIME g x as well, simply by noting that f = g, and x = x, and therefore RUNTIME f x = RUNTIME g x as well by the usual extensionality rule that would also apply to RUNTIME.
Yes that's the problem.
Take factorial.
fun factorial :: "nat => nat" where
"factorial 0 = 1"
| "factorial (Suc n) = (Suc n) * factorial n
I can then define
fun factorial_10_hardcoded :: "nat => nat" where
"factorial 10 = 3628800"
| "factorial 0 = 1"
| "factorial (Suc n) = (Suc n) * factorial n"
Clearly `factorial_10_hardcoded = factorial` for all `x`. Hence `RUNTIME f x = RUNTIME g x`. `RUNTIME factorial_10_hardcoded 10 <= 1` and therefore `RUNTIME factorial 10 <= 1`. So that gives you constant time for any particular constant input. But it gets even worse!
factorial_hardcoded_a_b "nat => nat => nat => nat" where
"factorial_hard_coded_a_b a b x = if x=a then b else factorial x
And of course `RUNTIME factorial_hardcoded_a_b x b x <= 1`.
Then I can prove
FORALL n. EX b. factorial n = factorial_hardcoded_a_b n b n
which then means I can conclude `RUNTIME factorial n <= 1`.
Yes, factorial_10_hardcoded convinces me that RUNTIME is not a good idea, although it works actually as RUNTIME is supposed to work: Hardcoding the computed value for a given input is the ultimate optimisation.
Not sure about the factorial_hardcoded_a_b example, because you still need to get rid of the existential somehow, maybe via skolemisation b[n], but that does not really matter in light of factorial_10_hardcoded.
The typing rules for RUNTIME would have been simply that if f has type a_1 => ... => a_n => b for n >= 1, and x_i has type a_i, then RUNTIME f x_1 ... x_n has type b.
That would exclude the clearly problematic case RUNTIME x for n = 0, but it seems to me hardcoding is basically how you can get that case back in via extensionality.
Although, I am starting to wonder how bad the constant hardcoding case really is.
As I said before, it is to be expected: Providing a precomputed value is a very fast implementation!
I am not entirely convinced yet that it would damage what RUNTIME can say about variable inputs, so I guess a complete analysis of your hardcoded_a_b example is necessary after all.