Automatically checking function is polynomial time

Stream: general

[Praneeth Kolichala]

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 $n$. Currently, I just handle $n=1$, $n=2$, and $n=3$ 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 $n$). 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]

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]

What's the type of f here?

[Anand Rao]

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]

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