Comment by auggierose

2 hours 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.

1 comment

auggierose

dwohnitmok 10 minutes 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`.