Sponsor
National Science Foundation under Grant No. 1317249.
Published In
25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015)
Document Type
Post-Print
Publication Date
12-17-2015
Subjects
Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Artificial Intelligence (incl. Robotics), Discrete Mathematics in Computer Science
Abstract
Although functional as well as logic languages use equality to discriminate between logically different cases, the operational meaning of equality is different in such languages. Functional languages reduce equational expressions to their Boolean values, True or False, logic languages use unification to check the validity only and fail otherwise. Consequently, the language Curry, which amalgamates functional and logic programming features, offers two kinds of equational expressions so that the programmer has to distinguish between these uses. We show that this distinction can be avoided by providing an analysis and transformation method that automatically selects the appropriate operation. Without this distinction in source programs, the language design can be simplified and the execution of programs can be optimized. As a consequence, we show that one kind of equational expressions is sufficient and unification is nothing else than an optimization of Boolean equality.
Persistent Identifier
http://archives.pdx.edu/ds/psu/16550
Citation Details
Antoy, S., & Hanus, M. (2015). From Boolean Equalities to Constraints. Logic-Based Program Synthesis and Transformation
Included in
Computer Engineering Commons, Computer Sciences Commons, Electrical and Computer Engineering Commons
Description
Paper presented at the 25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015), Siena, IT, July 13-15, 2015. Subsequently published by Springer.