Lists

Lists: Concepts, Issues, and Designs

Lists

There are two constructor sets: nil & cons; and nil, ncons, & append
The lists are homogeneous lists (i.e., all the elements of a list are of the same type); hence, they differ from Lisp lists. Also, here car and cdr are defined on NE-List rather than List as in Lisp. The sequence function elt is used rather than nth because of a better type/sort fit: elt is restricted to the Nats less than the length of the list while nth is defined to be nil outside that range. The spec is in: list.re

ALists

Association lists done as a definitional extension of the instantiation of Lists by pairs of Dom, Cod. The definitions are formulated in such a manner that code can be generated in the current system. The primary issue here is to find an acceptable definition of alist-apply. The definition used is:

 definition of alist-apply is 
  axiom (equal ((embed 1) (alist-apply L-at-x))
               (alist-apply* ((relax defined-at?) L-at-x)))
 end-definition

where alist-apply* is defined so that it is total on (AList, Dom). This requires giving a value for those pairs <L x> where L is not defined-at? x. The is done by taking the Cod of alist-apply* to be the sum of the original Cod and ERROR and then using error-value if L is not defined-at x. (This is based on the spec partial-as-triv-defn-extn.re ) Note that it is provable that alist-apply (as defined) is total on the Defined-domain. The spec is in: alist.re

SpecWeb Index

Specs