Oct. 28th, 2016

akuklev: (ДР Цертуса 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.Read more... )

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 21st, 2017 03:51 pm
Powered by Dreamwidth Studios