“During” cannot be expressed by “after”

摘要

We prove that the operator ⊥ (“during”) is not expressible in first-order logics of programs based on the operator 〈 〉 (“after”), but it is expressible with the help of array assignments or rich tests. From this we deduce that array assignments add to the power of logics based on nondeterministic effective tree-schemes and that rich tests add to the power of logics based on flowcharts. The proof of the main theorem is based on a result of Furst, Saxe, and Sipser (in “Proc. 22nd Found. of Comput. Sci.,” 1981). Then it shows an example of how the Boolean circuit complexity theory may be applied to logics of programs.