In the past decade, numerous attempts have been made to combine functional languages and logic languages into a single framework. But, there have been few languages which are both efficient enough to be widely used in many applications and mathematically clear. Some languages such as LOGLISP and POPLOG emphasize efficiency and the ease of developing programs without concerning about the denotational semantics of the combination. Hence, these languages are hardly considered to be logical extensions of LISP or Prolog. On the other hand, some languages such s Eqlog are mathematically clear, but very inefficient mainly owing to their complete inference rules.
This thesis aims at designing a typed functional logic language, called Tyflog. To achieve efficiency, Canonical unification is introduced as kind of E-unification algorithm to evaluate functions in a given equational theory. Based on Canonical unification, SLDC-resolution (SLD-resolution with Canonical unification) is presented as the run-time computation rule of Tyflog.
The functional logic part of Tyflog has two denotational semantics based on the extended Herbrand universe. Furthermore, SLDC-refutation is proved to be sound and complete with respect to these denotational semantics. Tyflog also provides polymorphic typing and detects type errors at compile time. Therefore, it can help reduce type errors which may otherwise appear at run time and delay software development process. These features make Tyflog suitable for a specification language.
1980년 이래 함수언어와 논리언어를 결합시키려는 시도가 진행되어 왔다. 그러나, 지금까지 대부분의 연구는 너무 이론적이어서 실제 사용하기에는 성능이 너무 떨어지거나 혹은 사용의 편리를 지나치게 강조하여 본래 함수언어나 논리언어가 가지고 있는 장점을 잃어버리는 경우가 대부분이었다. 예를 들어 LOGLISP이나 POPLOG와 같은 언어는 지나치게 사용의 편리를 강조하여 두가지 언어를 합친 의미가 모호하게 되었다. 한편, Eqlog와 같은 언어는 의미적으로는 명확하지만 수행 방식이 너무 복잡하여 매우 비효율적이다.
본 논문에서는 함수논리언어의 이러한 한계를 극복하고자 효율적이면서 의미적으로 명확한 언어인 Tyflog를 설계하였다. Tyflog의 효율성을 위하여 E-unification의 일종인 Canonical unification을 제안하였으며, Canonical unification을 기초로하여 Tyflog의 수행방식인 SLDC-resolution (SLD-resolution with Canonical unification)을 개발하였다.
본 논문에서는 Tyflog에 확장된 Herbrand universe를 기초로하여 두 가지의 denotational semantics를 부여하고 있는데, Tyflog의 수행방식은 이 의미론에 비추어 완전성이 증명되었다. Tyflog는 Polymorphic typing을 제공하고 있으며, 컴파일시에 type 에러를 찾아낸다. Tyflog의 이러한 특성은 수행 시에 발생할 수 있는 에러를 방지해 주는데, 소프트웨어의 개발시간을 단축하는데 큰 도움을 준다.
