Proving the Equivalence of Higher-Order Terms by Means of Supercompilation

One of the applications of supercompilation is proving properties of programs.We focus in this paper on a specic task: proving term equivalence for a higher-order lazy functional language. The \classical" way to prove equivalence of two terms t1 and t2 is to write an equality function equals and to simplify the term (equals t1 t2). However, this works only when certain conditions are met. The paper presents another approach to proving term equivalence by means of supercompilation. In this approach we supercompile both terms and compare supercompiled terms syntactically. Some applications of the technique are discussed. In particular, one of these applications may lead to the development of a more powerful \higher-level" supercompiler.

• Type: Conference
• Year: 2009
• Where: ERSHOV
• Authors: Ilya Klyuchnikov, Sergei A. Romanenko
• Attachments: 1 file(s)
• Keywords: ERSHOV 2009, Programming Languages