undefined | Better HN

0 pointsdwohnitmok3mo ago0 comments

This approach seems entirely unworkable.

You're saying that RUNTIME should be a built-in function, but then all the paragraphs succeeding that demonstrate that RUNTIME cannot be a function. All the typing judgments I can think of that would let RUNTIME become an actual function would lead to being able to prove false.

Moreover, RE

> RUNTIME for certain cases, and the theorems you generate must be inequalities, not equalities.

this is impossible under Isabelle's logic. I can easily turn any theorem about an inequality into a theorem about equality via an existential statement. E.g. given `RUNTIME f y <= n` I can easily write

  definition my_constant :: "nat" where
    "my_constant = (THE x. RUNTIME f y = x)"

which must logically exist by the classical nature of Isabelle. And now I get to work with `my_constant`. But I can always arbitrary force `my_constant` to be `1` or `0`. Because e.g. I can always just find another function `g` equal to `f` everywhere but just hard coding the answer for `y` (such that `RUNTIME` proves it to be less than or equal to `1`) and then prove `f = g` and then substitute it in, proving `my_constant` to be less than or equal to `1`.

In fact based on this definition of RUNTIME and Leibniz equality I could "prove" that every function runs in constant time. Because e.g. I can always make another append function `append_m_n` that hard codes what the result of `append` is on lists of constant size `m` and `n` and then I prove that `append_m_n` is equal to `append` and then I get to substitute it in every theorem because of equality so on and so forth.

Going down automatically generated `RUNTIME`s seems like a dead end. It seems to be missing some form of quantification over the implementation of a function, not just the function itself. And to the extent that functions do not have implementations, it doesn't seem you can retrofit formal runtime analysis.

0 comments

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

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

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

1 more reply

j / k navigate · click thread line to collapse

0 pointsdwohnitmok3mo ago0 comments

This approach seems entirely unworkable.

Moreover, RE

> RUNTIME for certain cases, and the theorems you generate must be inequalities, not equalities.

  definition my_constant :: "nat" where
    "my_constant = (THE x. RUNTIME f y = x)"

0 comments

auggierose3mo ago

dwohnitmokOP3mo 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?

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"

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

auggierose3mo ago

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.

1 more reply

j / k navigate · click thread line to collapse