We present an approach to theory exploration, i.e., a lemma synthesis procedure which discovers algebraic laws over recursive functions over Algebraic Data Types (ADTs). The approach, LemmaCalc, builds on, adapts and extends program calculation techniques known from optimization of functional programs (fusion and accumulator removal). Our approach avoids exponential search space of term enumeration (SyGuS) that can render state-of-the-art techniques prohibitively expensive or even useless on large theories with more than a handful of function symbols. In this paper we describe how this approach can be realized and contribute a robust implementation. The evaluation shows that different methods have complementary strengths and that each can produce lemmas not found by the other, but LemmaCalc scales much better to larger theories.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Quick Theory Exploration for Algebraic Data Types via Program Transformations

  • Gidon Ernst,
  • Grigory Fedyukovich

摘要

We present an approach to theory exploration, i.e., a lemma synthesis procedure which discovers algebraic laws over recursive functions over Algebraic Data Types (ADTs). The approach, LemmaCalc, builds on, adapts and extends program calculation techniques known from optimization of functional programs (fusion and accumulator removal). Our approach avoids exponential search space of term enumeration (SyGuS) that can render state-of-the-art techniques prohibitively expensive or even useless on large theories with more than a handful of function symbols. In this paper we describe how this approach can be realized and contribute a robust implementation. The evaluation shows that different methods have complementary strengths and that each can produce lemmas not found by the other, but LemmaCalc scales much better to larger theories.