Stream: Beginner Questions

Topic: Landau with arity > 1

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: Dec 07 2023 at 20:16 UTC