[r6rs-discuss] mathematical foundations

Thomas Lord lord at emf.net
Sun Jan 28 05:58:30 EST 2007


(Picking up on Sperber's thread but, from a different perspective.)

One design choice in Scheme concerns required procedures: should they 
ever be required to be total and effective over any of the fundamental 
types in Scheme?    For example, must eqv? always return either #t or #f?

The question is answered, I hope, by asking what a "fundamental type" in 
Scheme /is/.  I would first claim, uncontroversially I hope, that:

The fundamental types (booleans, numbers, characters, strings, and so 
forth) in Scheme form an axiomatically defined proper class equipped 
with a natural, albeit uncomputable equivalence relationship.   The 
required procedure eqv? is a sub-equivalence relationship: it returns #t 
only for truly equivalent values but may return #f even for truly 
equivalent values.    The most obvious evidence of this first claim is 
the question of equivalence among procedure objects.

(The "natural" equivalence relationship among Scheme values is 
substitutability of terms in an operational model of execution where 
"substitutability" can be defined in terms of "observable behaviors" 
such as operations on ports.)

Only slightly more controversially, I think, I would also claim that:

/Equivalence is not total and computable over _any_ of the disjoint types./

/*"Proof (by counterexample)":*/ /implicitly forced promises are an 
invited extension to the language./


One could similarly prove that the /type/ of an object is not total and 
computable.    Where the standard currently says something like "always 
returns an exact integer" or "always returns a boolean", that should 
really be interpreted as something like "never returns a value that is 
provably of any type defined as disjoint from [integers | booleans | etc.]".

Big yawn, right?   Except that it leaves us in some binds:

Suppose that the Report required eqv? to always return and always return 
#t or #f.   Then it is absolutely required, as a consequence, that eqv? 
sometimes give inaccurate results (false negatives).   This is 
unacceptable /as a requirement/, certainly, in the absence of a proof 
that it is inescapable in some convincing sense.

Suppose that an (execution of an) implementation /knows/ that eqv? has 
been called and passed  arguments for which it is unable to compute an 
accurate answer -- what should it do?    Surely, the report contains an 
unnecessary restriction if it /prohibits/ the implementation from 
returning a value whose semantics allow execution to continue without 
committing the implementation to an equivalence decision it is 
unprepared to make.

We can generalize that:  the report can not require that /any/ primitive 
procedure be total and computable.   This specifically precludes any 
procedure defined to "always" return either #t or #f or to always 
return, say, an exact integer (except in the weak sense that "exact 
integer" means "a value for which type predicates of types disjoint from 
exact integers never return true").

None of these statements change, at all, the reliably deterministic 
behavior of non-divergent Scheme programs.    What is changed, if we 
admit that /none/ of the primitive procedures can be given a total, 
computable specification, is what one can /prove/ about Scheme programs 
and how programs with no portably deterministic behavior behave.   
Useful proofs, in this interpretation of Scheme's types, can only prove 
relations between "nominal" input and output values -- proving effective 
totality over any reasonable class of fundamental Scheme types is 
definitionally ruled out.   And, so what:  it isn't the least charm of a 
portable program when one discovers it has a serendipitous yet well 
defined and completely explicable use when applied over unanticipated 
members of the classes of values it refers to.

Lisp is, in some sense, the ultimate pursuit of parsimony in programming 
-- it aims to be the language in which anything that only needs to be 
said once can be said, in fact, exactly once.   That is why it is 
defined as a (family of) languages in which all types are proper classes 
and all run-time values dynamically typed -- programs are procedures 
over /proper classes/ as such.   Scheme is, in some sense, a persistent 
attempt to express that essence of lisp simultaneously precisely and 
pragmatically, without /much/ commitment to compatibility with historic 
lisps (a commitment to preserve only arbitrary choices such as 
s-expression syntax).

And so: 

The report should not assert that #f is the only false value.

Eqv? should be permitted to return an unspecified value.

The result of any Scheme computation that is strict in some unspecified 
value should be unspecified.

If an implementation reifies unspecified values as such, it must not 
execute the program in any way that is strict with respect to the 
unspecified properties of the value.    For example,  (write (if 
(unspecified) 'a 'b))) should be an error while (write (begin (if 
(unspecified) 'a 'b) 'c))) should be permitted to print c.

-t

(Separately argued and on additional basis, but also supported here:  
char->integer should not be total.)



-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.r6rs.org/pipermail/r6rs-discuss/attachments/20070128/50ffec73/attachment.htm


More information about the r6rs-discuss mailing list