Guarded algebras: disguising partiality so you won't know whether its there

摘要

Motivated by considerations from program semantics, we suggest the notion of guarded algebras. These make explicit the significant arguments to functions, and prevent involuntary capture of error values and undefined cases in specifications. Here we show that guarded reasoning disguises whether the underlying models are partial or total.