Implementing Baker's SUBTYPEP decision procedure

From LRDE

Abstract

We present here our partial implementation of Baker's decision procedure for SUBTYPEP. In his article “A Decision Procedure for Common Lisp's SUBTYPEP Predicate”he claims to provide implementation guidelines to obtain a SUBTYPEP more accurate and as efficient as the average implementation. However, he did not provide any serious implementation and his description is sometimes obscure. In this paper we present our implementation of part of his procedure, only supporting primitive types, CLOS classesmember, range and logical type specifiers. We explain in our words our understanding of his procedure, with much more detail and examples than in Baker's article. We therefore clarify many parts of his description and fill in some of its gaps or omissions. We also argue in favor and against some of his choices and present our alternative solutions. We further provide some proofs that might be missing in his article and some early efficiency results. We have not released any code yet but we plan to open source it as soon as it is presentable.

Documents

Bibtex (lrde.bib)

@InProceedings{	  valais.19.els,
  author	= {L\'eo Valais and Jim Newton and Didier Verna},
  title		= {Implementing Baker's \texttt{SUBTYPEP} decision procedure},
  address	= {Genova, Italy},
  booktitle	= {12th European Lisp Symposium},
  year		= 2019,
  month		= apr,
  abstract	= {We present here our partial implementation of Baker's
		  decision procedure for SUBTYPEP. In his article ``A
		  Decision Procedure for Common Lisp's SUBTYPEP Predicate'',
		  he claims to provide implementation guidelines to obtain a
		  SUBTYPEP more accurate and as efficient as the average
		  implementation. However, he did not provide any serious
		  implementation and his description is sometimes obscure. In
		  this paper we present our implementation of part of his
		  procedure, only supporting primitive types, CLOS classes,
		  member, range and logical type specifiers. We explain in
		  our words our understanding of his procedure, with much
		  more detail and examples than in Baker's article. We
		  therefore clarify many parts of his description and fill in
		  some of its gaps or omissions. We also argue in favor and
		  against some of his choices and present our alternative
		  solutions. We further provide some proofs that might be
		  missing in his article and some early efficiency results.
		  We have not released any code yet but we plan to open
		  source it as soon as it is presentable.},
  lrdestatus	= {accepted}
}