Open AccessFast and loose reasoning is morally correct
Author(s) -
Nils Anders Danielsson,
John Hughes,
Patrik Jansson,
Jeremy Gibbons
Publication year - 2006
Publication title -
acm sigplan notices
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.31
H-Index - 99
eISSN - 1558-1160
pISSN - 0362-1340
DOI - 10.1145/1111320.1111056
Subject(s) - partial function , computer science , semantics (computer science) , partial evaluation , relation (database) , programming language , equivalence (formal languages) , function (biology) , syntax , domain theory , functional programming , mathematics , discrete mathematics , artificial intelligence , database , evolutionary biology , biology
Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning. Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values, and all types are lifted, including the function spaces. A partial equivalence relation (PER) is then defined, the domain of which is the total subset of the partial language. For types not containing function spaces the PER relates equal values, and functions are related if they map related values to related values. 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 PER gives rise to a bicartesian closed category which can be used to reason about values in the domain of the relation. Copyright © 2006 ACM
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom