Incollection,
Correspondence between Operational and Denotational Semantics
Handbook of Logic in Computer Science, Vol 4, Oxford University Press, (1995)
Abstract
ly, an occurrence is just a finite sequence of elements from the set f 0; 1; 2 g. The set f 0; 1; 2 g of occurrences is ranged over by meta-variables ff; fi. We read M = ff as "the subterm of M occurring at ff". Such a subterm may or may not be defined. The concatenation of sequences ff and fi is written as ff ^I�? fi. The prefix ordering 6 is defined in the standard way: we say that ff 6 fi if and only if fi = ff ^I�? fl for some sequence fl. The empty sequence is written as ffl....
