An abstract interpretation for ML equality kinds

Carl A. Gunter, Elsa L. Gunter, David B. MacQueen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The definition of Standard ML provides a form of generic equality which is inferred for certain types, called equality types, on which it is possible to define a computable equality relation. However~ the standard definition is incomplete in the sense that there are interesting and useful types which are not inferred to be equality types but which nevertheless have a computable equality relation. In this paper, a refinement of the Standard ML system of equality types is introduced and is proven sound and complete with respect to the existence of a computable equality. The technique used here is based on an abstract interpretation of ML operators as monotone functions over a three point lattice. It is shown how the equality relation can be defined (as an ML program) from the definition of a type with our equality property. Finally, a sound, efficient algorithm for inferring the equality property which corrects the limitations of the standard definition in all cases of practical interest is demonstrated.

Original languageEnglish (US)
Title of host publicationTheoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings
EditorsAlbert R. Meyer, Takayasu Ito
PublisherSpringer-Verlag
Pages112-130
Number of pages19
ISBN (Print)9783540544159
DOIs
StatePublished - Jan 1 1991
Event1st International Conference on Theoretical Aspects of Computer Software, TACS 1991 - Sendai, Japan
Duration: Sep 24 1991Sep 27 1991

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume526 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other1st International Conference on Theoretical Aspects of Computer Software, TACS 1991
CountryJapan
CitySendai
Period9/24/919/27/91

Fingerprint

Abstract Interpretation
Equality
Acoustic waves
Mathematical operators
Monotone Function
Lattice Points
Refinement
Efficient Algorithms

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Gunter, C. A., Gunter, E. L., & MacQueen, D. B. (1991). An abstract interpretation for ML equality kinds. In A. R. Meyer, & T. Ito (Eds.), Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings (pp. 112-130). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 526 LNCS). Springer-Verlag. https://doi.org/10.1007/3-540-54415-1_43

An abstract interpretation for ML equality kinds. / Gunter, Carl A.; Gunter, Elsa L.; MacQueen, David B.

Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings. ed. / Albert R. Meyer; Takayasu Ito. Springer-Verlag, 1991. p. 112-130 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 526 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Gunter, CA, Gunter, EL & MacQueen, DB 1991, An abstract interpretation for ML equality kinds. in AR Meyer & T Ito (eds), Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 526 LNCS, Springer-Verlag, pp. 112-130, 1st International Conference on Theoretical Aspects of Computer Software, TACS 1991, Sendai, Japan, 9/24/91. https://doi.org/10.1007/3-540-54415-1_43
Gunter CA, Gunter EL, MacQueen DB. An abstract interpretation for ML equality kinds. In Meyer AR, Ito T, editors, Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings. Springer-Verlag. 1991. p. 112-130. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-54415-1_43
Gunter, Carl A. ; Gunter, Elsa L. ; MacQueen, David B. / An abstract interpretation for ML equality kinds. Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings. editor / Albert R. Meyer ; Takayasu Ito. Springer-Verlag, 1991. pp. 112-130 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{6c4eb1f8a2f64bf8b64bc9a7858f310a,
title = "An abstract interpretation for ML equality kinds",
abstract = "The definition of Standard ML provides a form of generic equality which is inferred for certain types, called equality types, on which it is possible to define a computable equality relation. However~ the standard definition is incomplete in the sense that there are interesting and useful types which are not inferred to be equality types but which nevertheless have a computable equality relation. In this paper, a refinement of the Standard ML system of equality types is introduced and is proven sound and complete with respect to the existence of a computable equality. The technique used here is based on an abstract interpretation of ML operators as monotone functions over a three point lattice. It is shown how the equality relation can be defined (as an ML program) from the definition of a type with our equality property. Finally, a sound, efficient algorithm for inferring the equality property which corrects the limitations of the standard definition in all cases of practical interest is demonstrated.",
author = "Gunter, {Carl A.} and Gunter, {Elsa L.} and MacQueen, {David B.}",
year = "1991",
month = "1",
day = "1",
doi = "10.1007/3-540-54415-1_43",
language = "English (US)",
isbn = "9783540544159",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "112--130",
editor = "Meyer, {Albert R.} and Takayasu Ito",
booktitle = "Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings",

}

TY - GEN

T1 - An abstract interpretation for ML equality kinds

AU - Gunter, Carl A.

AU - Gunter, Elsa L.

AU - MacQueen, David B.

PY - 1991/1/1

Y1 - 1991/1/1

N2 - The definition of Standard ML provides a form of generic equality which is inferred for certain types, called equality types, on which it is possible to define a computable equality relation. However~ the standard definition is incomplete in the sense that there are interesting and useful types which are not inferred to be equality types but which nevertheless have a computable equality relation. In this paper, a refinement of the Standard ML system of equality types is introduced and is proven sound and complete with respect to the existence of a computable equality. The technique used here is based on an abstract interpretation of ML operators as monotone functions over a three point lattice. It is shown how the equality relation can be defined (as an ML program) from the definition of a type with our equality property. Finally, a sound, efficient algorithm for inferring the equality property which corrects the limitations of the standard definition in all cases of practical interest is demonstrated.

AB - The definition of Standard ML provides a form of generic equality which is inferred for certain types, called equality types, on which it is possible to define a computable equality relation. However~ the standard definition is incomplete in the sense that there are interesting and useful types which are not inferred to be equality types but which nevertheless have a computable equality relation. In this paper, a refinement of the Standard ML system of equality types is introduced and is proven sound and complete with respect to the existence of a computable equality. The technique used here is based on an abstract interpretation of ML operators as monotone functions over a three point lattice. It is shown how the equality relation can be defined (as an ML program) from the definition of a type with our equality property. Finally, a sound, efficient algorithm for inferring the equality property which corrects the limitations of the standard definition in all cases of practical interest is demonstrated.

UR - http://www.scopus.com/inward/record.url?scp=85030244930&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85030244930&partnerID=8YFLogxK

U2 - 10.1007/3-540-54415-1_43

DO - 10.1007/3-540-54415-1_43

M3 - Conference contribution

AN - SCOPUS:85030244930

SN - 9783540544159

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 112

EP - 130

BT - Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings

A2 - Meyer, Albert R.

A2 - Ito, Takayasu

PB - Springer-Verlag

ER -