Marco Haucke (Nov 29 2022 at 14:07): Marco Haucke (Nov 29 2022 at 14:07):Hi,
I am trying to work with Landau_Symbols to argue about functions that take more than a single argument.
When doing something like
fun f1 :: "nat => nat" where
"f1 x = 2 * x"
lemma "f1 ∈ O(λx. x)"
(* some proof here *)
everything works as expected.
However, when I try:
fun f2 :: "nat => nat => nat" where
"f2 x y = 2 * (x + y)"
(* will not work *)
lemma "f2 ∈ O(λx y. x + y)"
I cannot proceed because No type arity fun :: real_normed_field. I've tired uncurrying and similar workarounds but I was not
successful. After looking into the source, I am starting to fear that what I'm trying to do is not possible... :(
Thus my question: Is it possible to use Landau_Symbols to argue about functions taking multiple arguments and if so, how? :sweat_smile:
Wenda Li (Nov 29 2022 at 14:56):I don't think Landau with arity > 1 will work with the current Isabelle setup. Nevertheless, what would be the definition of Big-O on a multivariate function?
Marco Haucke (Nov 29 2022 at 16:20):The definition itself is not a problem, see for example: https://en.wikipedia.org/wiki/Big_O_notation#Multiple_variables
The only option I can see right now is actually uncurrying the functions and defining some ordering (order) on the tuples that makes sense. I'm not sure about that atm. I'll update the topic as I get more results :)
Marco Haucke (Nov 30 2022 at 22:20):I have a solution using tuples, (courtesy of @Manuel Eberl , thanks again) using the Product-Filter ×⇩F:
lemma "(λ(x, y). f2 x y) ∈ O[at_top ×⇩F at_top](λ(x, y). x + y)"
Last updated: Apr 26 2024 at 20:16 UTC