[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#6878: boolvectors of length 0 signal error when aref/aset the 0th e
From: 
MON KEY 
Subject: 
bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element 
Date: 
Thu, 19 Aug 2010 13:06:58 0400 
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 (makeboolvector 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)boolvectors")

 A boolvector 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 boolvector, 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
boolvectors 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 "BoolVector Type"
,

 A "boolvector" is a special type of onedimensional array. An elment
 of a boolvector which is accesible by its nonzero index must only be
 `t' or `nil'.

`
at info node "Boolvectors"
,

 A boolvector 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
 boolvector, the effect is to store `t' there. As with all arrays,
 boolvector indices start from 0. Emacs allows creation of a boolvector of
 length 0 however its length cannot be changed once the boolvector is created.
 An error is singaled if you try to access the 0 index of a boolvector of
 length 0. Boolvectors are constants when evaluated.

`

/s_P\
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, MON KEY, 2010/08/18
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, Stefan Monnier, 2010/08/18
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, MON KEY, 2010/08/18
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, Andreas Schwab, 2010/08/19
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, MON KEY, 2010/08/19
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, Stefan Monnier, 2010/08/19
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element,
MON KEY <=
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, Stefan Monnier, 2010/08/19
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, Andreas Schwab, 2010/08/19
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, Chong Yidong, 2010/08/19
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, MON KEY, 2010/08/19
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, Juanma Barranquero, 2010/08/19
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, Chong Yidong, 2010/08/19
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, MON KEY, 2010/08/19
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, Juanma Barranquero, 2010/08/19
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, MON KEY, 2010/08/20
 bug#6878: boolvectors of length 0 signal error when aref/aset the 0th element, Juanma Barranquero, 2010/08/20