Graph reduction is a fundamental way to implement lazy functional languages. However, it requires considerable heap space to store the intermediate graphs. This thesis presents a space efficient graph reduction machine called ZG-machine. The ZG-machine is a variant of the G-machine, which is an efficient graph reduction machine developed by Augustsson and Johnsson. The ZG-machine exploits a simple encoding method, called tag-forwarding, to compress the heap structure of graphs. Tag-forwarding reduces the size of the subgraph which can be allocated at the same time.
This thesis also proves that the ZG-machine is correct with respect to the G-machine. Lester showed the correctness of the G-machine by constructing a stack semantics in context of denotational semantics. In this thesis, the stack semantics of the ZG-machine is defined and it is proved to be congruent to the stack semantics of the G-machine. To show the equivalence of the abstract machine states, a standard graph notation is suggested. The standard graph denotes the essential graph information of the abstract machine states. The graph information of the abstract machine states can be projected to the standard graph domain and the congruence of the semantics can be proved on the basis of state equivalence.
To evaluate the performance of the ZG-machine, the G- and the ZG-machines are implemented as C translators. A source program is translated into two versions of C programs by the translators and the performance of the machines are measured by executing the C programs. According to the experimental results, the ZG-machine can reduce the total heap allocation by 27% and the heap residency by 34% on average compared to the G-machine. But, the run-time of the ZG-machine is increased by 34% when the heap constraint is severe. The high rate of the run-time overhead of the ZG-machine is incurred by the garbage collector. However, when the heap size is 7 times the heap residency, the run-time overhead of the ZG-machine is no more than 12% compared to the G-machine. With aspect of reduced heap residency, the ZG-machine may be useful in memory-restricted environments such as embedded systems. Also, with the development of a more efficient garbage collector, the run-time is expected to decrease significantly.
그래프 축약 방법은 지연 함수형 언어의 대표적인 구현 방법이다. 특히 G-machine은 빠른 그래프 축약을 수행하는 추상 기계로 많은 주목을 받아 왔다. 그러나, G-machine을 비롯한 그래프 축약 기계는 축약 과정에 생성되는 그래프를 저장하기 위해 많은 기억 장소를 필요로 한다. 본 논문은 G-machine의 그래프를 압축하여 저장하는 방법을 제시한다. G-machine 그래프에서 동시에 할당되는 부분에 대하여 태그를 링크와 함께 저장하여 옮김으로써 보다 적은 공간에 같은 정보를 가진 그래프가 저장되도록 한다. 이렇게 그래프를 압축하여 저장하는 방법을 태그 옮김이라고 하는데, 본 논문에서는 G-machine에 태그 옮김 기법을 적용하여 새로운 추상 기계 ZG-machine을 정의한다.
ZG-machine을 이용한 함수형 언어의 구현이 정확하다는 것은 G-machine의 정확성에 의거하여 증명할 수 있다. Lester는 G-machine의 정확성을 스택 의미정의를 통하여 증명한 바 있다. 본 논문에서는 간단한 언어에 대하여 두 추상 기계의 스택 의미를 정의하고, 스택 의미정의에 따라 두 추상 기계가 같은 출력값을 생성한다는 것을 보임으로써 ZG-machine의 정확성을 증명한다. 주어진 프로그램에 대해 두 추상 기계가 동등한 축약 과정을 거친다는 것을 보이기 위해 두 추상 기계의 상태의 동등함을 나타내는 방법이 필요한데, 이를 위해서 본 논문에서는 표준 그래프 표기법을 제안한다. 두 추상 기계의 상태로부터 표준 그래프로의 변환 함수를 기술하고, 이들이 같은 표준 그래프로 변환된다는 것을 보임으로써 두 추상 기계의 상태가 그래프 정보의 관점에서 동등함을 나타낸다.
구체적인 ZG-machine의 성능을 알아보기 위해 실험 체계를 구현하여 실험 결과를 알아본다. 실험 체계로 G-machine과 ZG-machine의 C 시뮬레이터를 구현하고, 이 시뮬레이터 상에서 간단한 벤치마크 프로그램에 대하여 두 추상 기계의 시간 효율과 공간 효율을 측정한다. ZG-machine의 성능을 G-machine에 대한 증가율로 측정해 볼 수 있는데, 실험 결과에 따르면 ZG-machine은 G-machine에 비하여 총 힙 사용량은 평균 27%, 최소 힙 사용량은 평균 34% 절약할 수 있는 것으로 나타났다. 그러나, ZG-machine의 프로그램 수행 시간은 다소 증가되었는데, 이는 기억 장소 재활용 알고리즘의 차이 때문인 것으로 생각된다. ZG-machine의 수행 시간의 증가율은 주어진 힙 공간의 제약에 따라 다르게 나타났는데, 힙 공간의 제약이 완화됨에 따라 대략 10% 이내로 감소되었다. ZG-machine의 실제 사용을 위해서는 보다 효율적인 기억 장소 재활용 체계의 개발이 필요하다.
