A formal grammar for P? Let $P$ be the class of formal languages that have polynomial-time decider, i.e. for each $L\in P$ there exists a Turing-machine $T$ such that for each $w\in L$ machine $T$ decides if $w\in L$ in polynomial time wrt the length of $w$.

Is it possible to define a grammar (in any "reasonable" sense) that could be used to define exactly the languages in $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.