A Sound Strategy to Compile General Recursion into Finite Depth Pattern Matching

• Maycon J. J. Amaro Universidade Federal de Ouro Preto
• Samuel S. Feitosa Universidade Federal da Fronteira Sul
• Rodrigo G. Ribeiro Universidade Federal de Ouro Preto

Resumo

Programming languages are popular and diverse, and the convenience of programmatically changing the behavior of complex systems is attractive even for the ones with stringent security requirements, which often impose restrictions on the acceptable programs. A very common restriction is that the program must terminate, which is very hard to check because the Halting Problem is undecidable. In this work, we proposed a technique to unroll recursive programs in functional languages to create terminating versions of them. We prove that our strategy itself is guaranteed to terminate. We also formalize term generation and run property-based tests to build confidence that the semantics is preserved through the transformation. Our strategy can be used to compile general purpose functional languages to restrictive targets such as the eBPF and smart contracts for blockchain networks.

Palavras-chave: Program transformation, Recursion, Program generation