October 28th, 2016

ДР Цертуса 2011


(Ниженаписанное — спекулятивный черновик для внутреннего применения, приведённые утверждения пока даже не проверены, не говоря о формальных доказательствах.)

Purely functional total computations are excellently understood both syntactically and semantically, they are very easy to work with mathematically. The business of describing effectful computations urges to extend this result from total pure functions to procedures written in powerful general purpose imperative programming languages. Procedures are assumed to be typed and composable (thus, form a category, say Proc; actually, a monoidal category we are to interpret procedures with more than one argument) and to faithfully include total pure functions (thus, there should be a monoidal functor proc : Func -> Proc). This structure is enough to interpret plain (i.e. without loops and other control structures) ALGOL-style procedure definitions, i.e. sequences of instructions and let-definitions. Control structures have to be described separately as additional generators of the Proc category.Collapse )