Bitstream Example

BitStreams are potentially infinite in length. The elements of this domain are finite sequences that have not yet been completed. So we can think of these elements as approximations to the actual bitstream.

These BitStream representations are semidecidable, we can determine if two representations of streams are not equal but we cannot determine if they are equal. So if two streams are not unequal it does not follow that they are equal.

We cannot determine if they are equal because, however many terms of two streams that start with the same values we have, they might be still be extended with different values. We can never check the complete bitstream because we cannot hold an infinite structure in a finite computer.

An example of a frame taken from Vickers section 3.7 example
It may help to think of the structure as recursive? bitstream recursive

My initial code for this is on github here.

(1) -> a := starts("011")

   (1)  starts:011
                                                         Type: BitStreamFrame
(2) -> b := starts("001")

   (2)  starts:001
                                                         Type: BitStreamFrame
(3) -> a /\ b

   (3)  starts:011
                                                         Type: BitStreamFrame
(4) -> 

I think perhaps the code should be changed to have an explicit terminator (as in Winskel)? If the following streams are terminated, then we can say the following is true:

101 <= 101110

Where <= means 'is subset of', that is, it starts in the same way.

but if the streams are not terminated, we can only say maybe, not true.

101 <= 101110

because the streams may be extended to be different.







metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.