Characterizing Inductive Theorems by Extensional Initial Models in a Higher-Order Equational Logic

概要

論文の詳細を見る
Term rewriting systems (TRSs) are an operational model for functional programming languages. Using TRSs, many interesting properties which programs should guarantee can be formally dealt with as inductive theorems. By introduction of higher-order functions which can deal with a function as an argument or a value, functional programming languages realize high-level abstraction and has heightened the expressive power. Since TRSs cannot express higher-order functions, we designed simply-typed TRSs (STRSs), which can express higher-order functions directly. In this presentation, we syntactically define the notion of inductive theorems in symply-typed systems. Next, the notion of algebraic models is also extended so that higher-order functions can be treated. Then we show that the notion of inductive theorems which we proposed corresponds to the external initial model semantics in this extended algebraic model. Lastly, we discuss the inductionless induction method based on our algebraic model, which provides a useful automated technique for proving inductive theorems in symply-typed systems. (Presented October 15, 2003)
一般社団法人情報処理学会の論文
2004-05-15