Definitions in nonstrict positive free logic. (English) Zbl 0876.03013

Gumb, Raymond D.; Lambert, Karel

Mod. Log. 7, No. 1, 25-55 (1997); errata ibid. 7, No. 3-4, 435-440 (1997).

Summary: Every “practical” programming language supplies the programmer with at least one nonstrict construct, such as the ALGOL60 arithmetic ‘if-then-else’ and the LISP ‘cond’. Many programming languages also enable the user to define nonstrict functions. In some languages, this is accomplished through the lazy evaluation of procedure parameters, as realized, for example, by the call-by-name devices of ALGOL60 and SIMULA67 and the call-by-need mechanism of Haskell. In other languages, such as Common LISP, a macro definition facility can serve a similar purpose. Programming languages that provide a mechanism for the user to define nonstrict functions are nonstrict languages, and we call the natural underlying logic of these languages nonstrict positive free logic. In this paper, we present the definition theory of nonstrict positive free logic. Suitable transformations of sentences in standard logic into sentences in nonstrict positive free logic preserve many properties of definitions in standard logic.

MSC:

03B70	Logic in computer science
68N15	Theory of programming languages

Keywords:

nonstrict programming languages; nonstrict functions; nonstrict positive free logic; definition theory; transformations of sentences

Software:

Simula 67