Completeness of the Reduced Form

Abstract

The reduction algebra defined in the previous chapter can be thought of as taking in a stream of characters and spitting out a transformed stream of characters. It is important to establish that this algebra can successfully reduce the input stream to a reduced normal form that cannot be further reduced by the algebra (irreducibility property). It is also useful to establish that if the reduction algebra can take two different paths in reducing the input stream, both paths lead to the same final reduced form (completeness property). Intuitively, our reduction algebra seems to have both of the above properties since all reduction functions except SA-REDUCE output a process statement on which only SA-REDUCE can be applied. Once SA-REDUCE is applied, there are no further reductions. The following sections prove the above properties formally through an embedding of the reduction algebra in the automated proof checker PVS. The following sections presents a brief introduction to PVS and the embedding of the algebra in PVS.