A formal grammar for P?
If you have notions of linear logic, you might want to have a look at the article Soft Linear Logic and Polynomial Time [1] that describes a variant of linear logic (some of the deduction rules have been modified) whose formulas are only provable by proof that are polynomial-time algorithm.

[1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.1196

Abstract: We present a subsystem of second order Linear Logic with restricted rules for exponentials so that proofs correspond to polynomial time algorithms, and vice-versa.