Zulip Chat Archive
Stream: general
Topic: Automatically checking function is polynomial time
Praneeth Kolichala (Aug 07 2022 at 05:39):
Hey everyone,
I've been working on a small project recently to formalize polynomial time complexity. You can check it out here: https://github.com/prakol16/lean_complexity_theory_polytime_trees.
I have a tactic polyfun
which tries to automatically prove that functions run in polynomial time. The core idea of the tactic is to split a goal of the form
⊢ polytime_fun (λ x, f (g₁ x) (g₂ x) ... (gₙ x))
into
⊢ polytime_funₙ f
⊢ polytime_fun g₁
...
⊢ polytime_fun gₙ
Note that polytime_funₙ f
is by definition polytime_fun (λ (x : α₁ × ⋯ × αₙ), f x.1 x.2 ... x.n)
.
I'm still new to tactic writing so I need some help.
One issue with this is that it doesn't generalize well based on . Currently, I just handle , , and each with their own lemma (although this is all I've needed so far, and it isn't terribly hard to add a few more lemmas for larger ). I'm not sure if there is a better way though.
Another issue is determining how many parameters there are. In particular we need to ignore arguments that just supply e.g. the type, or instances. The way I do this currently is search for a pencodable
instance on each argument. For example, if the goal was
⊢ polytime_fun (λ (m n : list α), m ++ n)
then it should split this into goals saying that list.append
is a polytime_fun₂
and projections are. However, there is an implicit argument to list.append
(namely, α
) which should be ignored. In this case, it is ignored because Type u
(the type of α
) does not have a polycodable
instance.
However, I'm worried about performance here -- is there a better way to infer which arguments are "true" arguments and which are likely just auxiliary information?
Violeta Hernández (Aug 08 2022 at 02:21):
You could try using docs#arity to generalize this to however many variables, but do note that this has very little use throughout mathlib
Eric Wieser (Aug 08 2022 at 09:56):
What's the type of f
here?
Anand Rao (Aug 09 2022 at 17:48):
Would an approach based on typeclass inference work here? This is a rough outline of what I had in mind:
/- A typeclass for polynomial-time functions.
To make the typeclass inference work smoothly, the class `polytime` is defined for terms of arbitrary types rather than only for simple function types. -/
class polytime {α : Type*} (a : α)
-- the definition of a polynomial time function goes here
/- The value of a polynomial-time function at any input is still a polynomial time function -/
instance polytime_eval {α β : Type*} (f : α → β) [polytime f] (a : α) [polytime a] : polytime (f a) := sorry
/- The composition of polynomial-time function is polynomial-time -/
instance polytime_comp {α β γ : Type*} (f : β → γ) [polytime f] (g : α → β) [polytime g] : polytime (λ x, f (g x)) := sorry
/- The application of a polynomial-time function to a polynomial-time argument is polynomial-time -/
instance polytime_app {α β γ : Type*} (f : Π (a : α), β → γ) [polytime f] (b : β) [polytime b] :
polytime (λ x, f x b) := sorry
And here are some specific examples of inference in action:
def nat.sq (n : ℕ) : ℕ := n^2 -- squares a natural number
/- The identity function is polynomial-time -/
instance {α : Type*} : polytime (@id α) := sorry
/- The function `nat.sq` is polynomial-time -/
instance : polytime (nat.sq) := sorry
/- Addition of natural numbers is polynomial-time -/
instance : polytime nat.add := sorry
/- Every natural number is polynomial time (one way to make sense of this is that every constant is a 0-ary function that can be evaluated in a fixed amount of time) -/
instance nat_polytime (n : ℕ) : polytime n := sorry
-- here the `α` in `id α` is ignored and only the relevant parameters are considered
instance eg_infer : polytime (λ n, nat.sq (id n)) := infer_instance
-- a bit more work is required here, but this complicated is still derivable from typeclass inference
instance eg_multi_arg : polytime (λ n, (nat.add (nat.sq n)) 5) := by {
show polytime (λ n, ((λ x, nat.add (nat.sq x)) n) 5),
apply_instance,
}
This is by no means a complete solution, but I think it addresses some parts of the question (such as ignoring implicit arguments). There may also be a better way to do this that avoids the show
in the last example, but I am not aware of one. I suspect that the three typeclass instances above will be enough to handle a wide variety of cases thanks to currying.
Eric Wieser (Aug 09 2022 at 19:23):
I'm pretty sure typeclass search won't work for comp
, as we had trouble with it on is_monoid_hom due to it performing higher order unification
Last updated: Dec 20 2023 at 11:08 UTC