Hardware and software co-design is a design technique which delivers computer systems comprising hardware and software components. A critical phase of the co-design process is to decompose a program into hardware and software. This paper proposes an algebraic partitioning algorithm whose correctness is verified in program algebra. The authors introduce a program analysis phase before program partitioning and develop a collection of syntax-based splitting rules. The former provides the information for moving operations from software to hardware and reducing the interaction between components, and the latter supports a compositional approach to program partitioning.