Operational and Denotational Semantics Describing the Matching Process in SNOBOL4

摘要

The pattern matching process in SNOBOL4 is investigated. A subset of the language which is simple in that patterns are not allowed as values of variables is considered. This leads to matching processes that always terminate. An informal description of the matching algorithm and an operational semantics in the SECD-machine style are presented. This semantics uses a stack to implement backtracking which can occur during matching. A denotational semantics is introduced which uses continuations to describe the backtracking. Equivalence of the two semantics is then proved. The operational and denotational semantics are as similar as possible while retaining the typical operational, respectively denotational ideas. This leads to a straightforward equivalence proof. That this similarity pays off is shown by another, somewhat disparate operational semantics for which equivalence with the denotational semantics is much harder to prove.