| "Judgements" for Syntactic Definition of Fixpoint Programs (2007) | |||||||||||||
Abstract | |||||||||||||
| In order to give a precise syntactic definition of fixpoint programs, we introduced "judgements" similar to those used in typed #-calculus. Hoare-He-Sanders[1] gave the following inductive definition of the set of commands as a set of binary relations on a given set S. This definition is parameterised by a family of binary relations { R i | i # I }. . R i (i # I) is a command. . skip is a command. . abort is a command. . If R, R # are commands, R; R # (the composition of R and R # as relations) is a command. . If R and R # are commands, R # R # (the union of R and R # as sets) is a command. . If R j (j # N) is a descending chain of commands (i.e., if j # j # implies R j # R j # ), # j#N R j is a command. This contains an infinitary operator # , with which I am not happy. The purpose of introducing this infinitary operator, however, is to deal with fixpoint operators. So, we wish to replace the infinitary operator by the fixpoint operator fixX.C. But ... | |||||||||||||
Publication details | |||||||||||||
| |||||||||||||