분리 시스템의 람다 계산법으로의 변환

Translation of Separable Systems into the Lambda Calculus

본 연구에서는 패턴을 갖는 항 개서 체계(TRS, Term Rewriting Systems)의 룰을 람다 계산법으로 코딩하는 변환 방법을 제시한다. Böhm의 분리성 이론에 따라 차별화된 룰 패턴을 갖는 분리 시스템은 람다 계산법으로 변환될 수 있음을 보인다. 또한, Böhm 동등 부류의 특성을 적용함으로써, 이 변환은 디폴트 룰로 된 개서 시스템을 코딩할 수 있으며 TRS의 '의미 없는 팀'들을 동일한 람다 팀으로 해석할 수 있도록 한다.

This research presents an translation technique of encoding rewrite rules with patterns into the lambda calculus. We show, following the theory of Böhm separability, rewrite rules with distinctive patterns, called separable systems, can be translated into the lambda calculus. Moreover, according to the property of Böhm equivalence classes, we can also encode rewrite systems with default rules, which allows to interpret some of 'undefined' terms of TRSs as an identified lambda term.