Abstract interpretation was introduced as a framework for construction of static analysis of computer programs. Abstract interpretation can be regarded as a partial execution of programs with information about its semantics and without performing all the computation. Originally abstract interpretation was applied to static analysis of programs. However it turned out that abstract interpretation also can be used in representing the relationships between various formal semantics which are expressed by fixpoint semantics. On the other hand, it is well known that a context free grammar can be regarded as a kind of deductive system. Moreover it is also known that a deductive system can expresses a fixpoint semantics. Based on these two ideas, it is possible to represent a semantics of a given context free grammar by a fixpoint semantics and express a parser of the grammar with an abstract interpretation of the semantics of the grammar. Cousot and Cousot represented Earley's parsing algorithm as an abstract interpretation in their research, and they expected that it would be possible to express other parsing algorithms with similar method.
On the other hand, $LR(\kappa)$ parsing is the strongest deterministic parsing algorithm, and $LL(\kappa)$ parsing is a top-down dual of $LR(\kappa)$ parsing. These are among the strongest deterministic parsing algorithms and used widely in practical applications. Nonetheless the theory of construction of these parsing algorithms is not understood widely. While most textbooks of compiler construction or automata theory mention LR parsing, the correctness proofs of the construction algorithms of LR parsers and LR parsing algorithms are omitted usually. Even in the texts which describe the theory and proofs in detail, developments of the theory are mainly procedural and it is not easy to understand them intuitively.
In this research, after the line of Cousot and Cousot's works, we represented $LR(\kappa)$ and $LL(\kappa)$ parsing algorithms as abstract interpretations. In order to do so, we expressed LR and LL validness concepts, which are essential in construction of LR and LL parsing, with fixpoint semantics and represented the fixpoint semantics as abstract interpretations of semantics derived from a given grammar. Semantics of LR and LL validness concept can be expressed in two ways. One is to follow their formal definitions and the other is to follow the derivations of reverse direction than the formal definitions. The algorithms to compute LR and LL validness can be derived from the semantics of the reverse direction directly. Expressed by fixpoint semantics, their equality is easy to understand intuitively, and the proofs of equality, done by simple inductions, hold almost mechanically. Therefore fixpoint semantics provides some easier to understand proofs of correctness of the LR and LL algorithms. In this research, we also showed that $LR(\kappa)$ and $LL(\kappa)$ parsers are expressed as abstract interpretations of semantics derived from a grammar. These abstract interpretations help the correctness proofs of $LR(\kappa)$ and $LL(\kappa)$ parsers.
Extending theses examples, we can expect that the abstract interpretation method can be used as a general framework of parsing representation. In this research we showed that parsing schemata, a parsing framework introduced by Sikkel, and the relationships between parsing schemata can be represented by the abstract interpretation method. Also it is shown that in most cases we can use the proof technique which was used in the cases of Earley's parsing and $LR(\kappa)$ and $LL(\kappa)$ parsing.
요약해석은 프로그램의 정적 분석을 구성하기 위한 구성하기 위한 기반으로서 도입되었다. 요약해석은 컴퓨터 프로그램의 의미론에 대한 정보에 기반하여 프로그램이 지시하는 모든 계산을 행하지 않고 부분적으로 실행하는 것이라고 볼 수 있다. 요약해석은 원래 프로그램 정적 분석에 응용되었으나, 한편 고정점 의미론에 의해 표현되는 다양한 종류의 프로그램 언어 의미론 사이의 관계를 표현하는 데에도 사용될 수 있다는 것이 밝혀졌다. 다른 한편 문맥자유문법을 일종의 연역 체계로 해석할 수 있다는 것은 잘 알려져 있는 사실이며, 어떤 연역 체계가 고정점 의미론을 표현할 수 있다는 것도 알려져 있는 사실이다. 이러한 두 아이디어에 기반 하여, 주어진 문맥자유문법의 의미론을 고정점 의미론으로 표현하고, 그 문법의 구문 분석을 문법의 의미론의 요약해석으로 표현하는 것이 가능하다. Cousot와 Cousot는 그들의 연구에서 Earley의 구문분석 알고리즘을 요약해석으로 표현하였으며, 또한 비슷한 방법으로 다른 구문분석을 표현하는 것도 가능할 것이라 예측하였다.
다른 한 편, $LR(\kappa)$ 구문분석은 가장 강력한 결정적 구문분석 알고리즘이고, $LL(\kappa)$ 구문분석은 $LR(\kappa)$ 구문 분석과 같은 방법론을 하향식 구문분석에 채용한 구문분석 알고리즘이다. 이들은 결정적 구문분석 알고리즘 중 가장 강력한 것들로서, 실용적으로 널리 사용되고 있는 구문분석 알고리즘이다. 그럼에도 불구하고 이들 구문분석 알고리즘을 구성하는 이론은 그 중요성에 비해 널리 이해되고 있지 못하다. 대부분의 컴파일러구성이나 오토마타이론 교과서가 LR 구문분석을 언급하고 있으면서도, 그 구성 알고리즘의 정확성의 증명을 생략하고 있다. 이론과 증명을 상세하게 수록한 문헌들의 경우에도 그 전개는 주로 절차적이어서 직관적으로 이해하기 쉽다고 할 수 없다.
본 연구에서는 Cousot와 Cousot의 요약해석에 의한 방법론을 따라 $LR(\kappa)$ 와 $LL(\kappa)$ 구문분석을 표현하였다. 이를 위해 LR 구문분석과 LL 구분분석을 구성하는데 필수적인 LR 및 LL 유효성 (validness) 개념을 고정점 의미론으로 표현하고 이것들을 주어진 문법에서 도출된 의미론의 요약해석으로 표현하였다. LR 및 LL 유효성 개념을 표현하는 의미론은 두 가지 방법으로 표현될 수 있다. 하나는 유효성의 형식적 정의를 그대로 따른 것이고, 다른 하나는 그 형식적 정의에서 따르는 문법상의 유도 (derivation) 의 방향을 반대로 바꾼 것이다. LR 및 LL 유효성을 계산하는 알고리즘은 이 반대 방향의 의미론에서 곧바로 도출할 수 있다. 고정점 의미론으로 표현되었을 때 이들이 같음은 직관적으로 매우 이해하기 쉽게 표현되며, 그 증명도 단순한 귀납법의 방법으로 거의 기계적으로 성립한다. 그러므로 고정점 의미론은 LR 및 LL 유효성을 계산하는 알고리즘의 정확성을 훨씬 이해하기 쉽게 증명하는 데 도움이 된다. 또한 본 연구에서는 LR 및 LL 구문분석 알고리즘들 또한 문법에서 도출된 의미론의 요약해석으로 표현됨을 증명하였다. 이 증명은 LR 및 LL 구문분석 알고리즘의 정확성을 증명하는데 도움이 된다.
이러한 사례들을 확장하면, 요약해석을 사용한 방법론이 구문분석을 표현하는 일반적인 프레임웍으로 사용될 수 있으리라 기대할 수 있다. 본 연구에서는 요약해석과 고정점 의미론에 기반한 방법으로 Sikkel 에 의해 도입된 구문분석 프레임웍인 파싱 스키마타와 파싱 스키마타 사이의 관계를 표현할 수 있으며, Earley의 구문분석과 LR 및 LL 구문분석에 대해 사용해 온 증명 기법도 대부분의 경우 사용할 수 있음을 보였다.
