# 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 $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 (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: Aug 03 2023 at 10:10 UTC