Fast and Loose Reasoning Is Morally Correct Export

@unpublished{citeulike:305371, abstract = {We justify reasoning about non-total (partial) functional languages using methods seemingly only valid for total ones; this permits "fast and loose" reasoning without actually being loose. Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values and lifted types, including lifted function spaces. A partial equivalence relation is then defined, the domain of which is the total subset of the partial language. It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language. It is also shown that the partial equivalence relation gives rise to a bicartesian closed category, which can be used to reason about values in the domain of the relation.}, author = {Danielsson, Nils A. and Gibbons, Jeremy and Hughes, John and Jansson, Patrik}, citeulike-article-id = {305371}, citeulike-linkout-0 = {http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast loose.pdf}, citeulike-linkout-1 = {http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast+loose.pdf}, keywords = {equational-reasoning, non-strict, semantics}, posted-at = {2005-08-27 05:05:22}, priority = {2}, title = {Fast and Loose Reasoning Is Morally Correct}, url = {http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast loose.pdf}, year = {2005} }

TY - UNPB ID - citeulike:305371 L3 - citeulike-article-id:305371 N2 - We justify reasoning about non-total (partial) functional languages using methods seemingly only valid for total ones; this permits "fast and loose" reasoning without actually being loose. Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values and lifted types, including lifted function spaces. A partial equivalence relation is then defined, the domain of which is the total subset of the partial language. It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language. It is also shown that the partial equivalence relation gives rise to a bicartesian closed category, which can be used to reason about values in the domain of the relation. TI - Fast and Loose Reasoning Is Morally Correct KW - equational-reasoning KW - non-strict KW - semantics AU - Danielsson, Nils AU - Gibbons, Jeremy AU - Hughes, John AU - Jansson, Patrik PY - 2005/// UR - http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast loose.pdf ER -