The lazy logic of partial terms

Journal of Symbolic Logic 67 (3):1065-1077 (2002)
The Logic of Partial Terms LPT is a strict negative free logic that provides an economical framework for developing many traditional mathematical theories having partial functions. In these traditional theories, all functions and predicates are strict. For example, if a unary function (predicate) is applied to an undefined argument, the result is undefined (respectively, false). On the other hand, every practical programming language incorporates at least one nonstrict or lazy construct, such as the if-then-else, but nonstrict functions cannot be either primitive or introduced in definitional extensions in LPT. Consequently, lazy programming language constructs do not fit the traditional mathematical mold inherent in LPT. A nonstrict (positive free) logic is required to handle nonstrict functions and predicates. Previously developed nonstrict logics are not fully satisfactory because they are verbose in describing strict functions (which predominate in many programming languages), and some logicians find their semantics philosophically unpalatable. The newly developed Lazy Logic of Partial Terms LL is as concise as LPT in describing strict functions and predicates, and strict and nonstrict functions and predicates can be introduced in definitional extensions of traditional mathematical theories. LL is "built on top of" LPT, and, like LPT, admits only one domain in the semantics. In the semantics, for the case of a nonstrict unary function h in an LL theory T, we have $\models_T h(\perp) = y \longleftrightarrow \forall x(h(x) = y)$ , where $\perp$ is a canonical undefined term. Correspondingly, in the axiomatization, the "indifference" (to the value of the argument) axiom $h(\perp) = y \longleftrightarrow \forall x(h(x) = y)$ guarantees a proper fit with the semantics. The price paid for LL's naturalness is that it is tailored for describing a specific area of computer science, program specification and verification, possibly limiting its role in explicating classical mathematical and philosophical subjects
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2178/jsl/1190150149
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history Request removal from index
Download options
PhilPapers Archive

Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 21,439
External links
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library
References found in this work BETA
Solomon Feferman (1995). Definedness. Erkenntnis 43 (3):295 - 320.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Monthly downloads

Added to index


Total downloads

12 ( #300,556 of 1,911,608 )

Recent downloads (6 months)

2 ( #321,691 of 1,911,608 )

How can I increase my downloads?

My notes
Sign in to use this feature

Start a new thread
There  are no threads in this forum
Nothing in this forum yet.