Legged locomotion arises from intermittent contact between limbs and terrain. Since it emerges from a closed-loop interaction, reductionist study of body mechanics and terrestrial dynamics in isolation have failed to yield comprehensive strategies for forward- or reverse-engineering locomotion. Progress in locomotion science stands to benefit a diverse array of engineers, scientists, and clinicians working in robotics, neuromechanics, and rehabilitation. Eschewing reductionism in favor of a holistic study, we seek a systems-level theory tailored to the dynamics of legged locomotion. Parsimonious mathematical models for legged locomotion are hybrid, as the system state undergoes continuous flow through limb stance and swing phases punctuated by instantaneous reset at discrete touchdown and liftoff events. In their full generality, hybrid systems can exhibit properties such as nondeterminism and orbital instability that are inconsistent with observations of organismal biomechanics. By specializing to a class of intrinsically self-consistent dynamical models, we exclude such pathologies while retaining emergent phenomena that arise in closed-loop studies of locomotion. Beginning with a general class of hybrid control systems, we construct an intrinsic state-space metric and derive a provably-convergent numerical simulation algorithm. This resolves two longstanding problems in hybrid systems theory: non-trivial comparison of states from distinct discrete modes, and accurate simulation up to and including Zeno events. Focusing on models for periodic gaits, we prove that isolated discrete transitions generically lead the hybrid dynamical system to reduce to an equivalent classical (smooth) dynamical system. This novel route to reduction in models of rhythmic phenomena demonstrates that the closed-loop interaction between limbs and terrain is generally simpler than either taken in isolation. Finally, we show that the non-smooth flow resulting from arbitrary footfall timing possesses a non-classical (Bouligand) derivative. This provides a foundation for design and control of multi-legged maneuvers. Taken together, these contributions yield a unified analytical and computational framework -- a hybrid dynamical systems theory -- applicable to legged locomotion.