bug#6878: bool-vectors of length 0 signal error when aref/aset the 0th element

[MON KEY <monkey@sandpframing.com>]

On Thu, Aug 19, 2010 at 11:51 AM, Stefan Monnier
<monnier@iro.umontreal.ca> wrote:
>> Prove it!
>
> Easy! formally, he said:
>
>  ∀ n ≥ 0 ∧ n < 0. (aref (make-bool-vector 0 t) n) ∈ { nil, t }
>
> And since there is no such `n', this is trivially true.
> More specifically, "n ≥ 0 ∧ n < 0" is a falsehood, and from false you
> can conclude anything you wish.  Among other things you can just
> a trivially prove:
>
>  ∀ n ≥ 0 ∧ n < 0. the sky is green
>

The problem with the above semantic vodoo is that it doesn't reflect the
contents of the manual either:

,---- (info "(elisp)bool-vectors")
|
| A bool-vector is much like a vector, except that it stores only the
| values `t' and `nil'.  If you try to store any non-`nil' value into an
| element of the bool-vector, the effect is to store `t' there.
|
`----

Informally, your formal proof is valid only so long as we suspend
belief in the manual and the sources which the manual is intended to
inform, specifically the place where it doesn't say that 0 length
bool-vectors don't have a value at index 0. IOW your proofs universal
qualifer relies on an empty domain where the manual would suggest
otherwise.  Since there is no "formal Emacs Lisp specification", and
since we are not discussing the formal realm of denotational semantics
nor first order logic w/ regards to a formal Emacs Lisp specification
your proof is indeed only trivially applicable.

Here is what I think the manual should say:

at info node "Bool-Vector Type"

,----
|
| A "bool-vector" is a special type of one-dimensional array.  An elment
| of a bool-vector which is accesible by its non-zero index must only be
| `t' or `nil'.
|
`----

at info node "Bool-vectors"

,----
|
| A bool-vector is a special type of vector which stores only the values `t'
| and `nil'.  If you try to store any non-`nil' value into an element of the
| bool-vector, the effect is to store `t' there.  As with all arrays,
| bool-vector indices start from 0. Emacs allows creation of a bool-vector of
| length 0 however its length cannot be changed once the bool-vector is created.
| An error is singaled if you try to access the 0 index of a bool-vector of
| length 0.  Bool-vectors are constants when evaluated.
|
`----


--
/s_P\