Comment by auggierose

2 months ago

RUNTIME would not be an actual function, but a built-in construct with its own typing rules that don't give RUNTIME a type, but only its applications. That's why you need to modify the type system, obviously. That is not a problem.

Yes, RUNTIME cannot talk about the implementation of a function, because there is no such thing as a unique implementation of a mathematical function. It will never be able to, it just computes upper bounds of runtime complexity based on the best implementations in the form of equations you can come up with. That on its own is not a dead end, that is the design. If you want to talk about implementations, you will need to come up with an explicit machine model, as mentioned a few times before now.

Your examples are a bit too handwavy for me to see exactly how you would come up with counter examples for the proper functioning of RUNTIME. I've played around with it a bit as well, and while counter intuitive in some aspects (for example RUNTIME append ys [] <= 1 could also be shown) it encodes an interesting notion of "optimal runtime" of a mathematical function. I might be wrong though, but you'd need to come up with an actual concrete example to convince me of that. For example, how exactly would you "hardcode" a value for g at y such that g y = f y = arbitrary constant you choose? You can show g y = f y = my_constant, but how does that help you to prove my_constant <= 1? "y" is just a constant as well, it cannot be a variable, because otherwise your definition of my_constant would not be closed. Note that equalities including THE would not yield anything usable from the inequalities generator.

Furthermore, note that just because f x = g x may hold for some x, that does not mean you can prove RUNTIME f x = RUNTIME g x for that x. 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.

3 comments

auggierose

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`.

auggierose 2 months ago
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.
- auggierose 2 months ago
  
  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.