Substitution: Syntactic versus Semantic
1998-004 |
The Fifth Internatinal Conference on Theoretical and Methodological Issues in Machine Translation with special emphasis on: MT in the Next Generation
What I find to be the one subtle and somewhat ugly part of TLA involves substitution in Enabled predicates. In the predicate Enabled A, there is an implicit quantification over the primed variables in A. Hence, mathematical substitution does not distribute over the Enabled operator. This four-page note explains that the same problem arises in most program logics because there is also an implicit quantification in the sequential-composition (semicolon) operator, so substitution does not distribute over semicolon. Apparently, no one had noticed this before because they hadn’t tried using programming logics to do the sort of things that are easy to do in TLA.