A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic