Programmatic Manipulation of Common Lisp Type Specifiers

Authors

Jim Newton, Didier Verna, Maximilien Colange

Where

European Lisp Symposium

Place

Brussels, Belgium

Type

inproceedings

Projects

Climb

Keywords

Graph algorithms, typechecking, Boolean functions, Binary decision diagrams, data structures

Date

2017-02-06

Abstract

In this article we contrast the use of the s-expression with the BDD (Binary Decision Diagram) as a data structure for programmatically manipulating Common Lisp type specifiers. The s-expression is the de facto standard surface syntax and also programmatic representation of the type specifier, but the BDD data structure offers advantages: most notably, type equivalence checks using s-expressions can be computationally intensive, whereas the type equivalence check using BDDs is a check for object identity. As an implementation and performance experimentwe define the notion of maximal disjoint type decomposition, and discuss implementations of algorithms to compute it: a brute force iteration, and as a tree reduction. The experimental implementations represent type specifiers by both aforementioned data structures, and we compare the performance observed in each approach.

Documents

• Paper

• Slides

See also the Technical Report with many more details.

Bibtex (lrde.bib)

@InProceedings{	  newton.17.els,
  author	= {Jim Newton and Didier Verna and Maximilien Colange},
  title		= {Programmatic Manipulation of {C}ommon {L}isp Type
		  Specifiers},
  booktitle	= {European Lisp Symposium},
  year		= 2017,
  lrdestatus	= {accepted},
  address	= {Brussels, Belgium},
  month		= apr,
  abstract	= {In this article we contrast the use of the s-expression
		  with the BDD (Binary Decision Diagram) as a data structure
		  for programmatically manipulating Common Lisp type
		  specifiers. The s-expression is the de facto standard
		  surface syntax and also programmatic representation of the
		  type specifier, but the BDD data structure offers
		  advantages: most notably, type equivalence checks using
		  s-expressions can be computationally intensive, whereas the
		  type equivalence check using BDDs is a check for object
		  identity. As an implementation and performance experiment,
		  we define the notion of maximal disjoint type
		  decomposition, and discuss implementations of algorithms to
		  compute it: a brute force iteration, and as a tree
		  reduction. The experimental implementations represent type
		  specifiers by both aforementioned data structures, and we
		  compare the performance observed in each approach.}
}