diff --git a/docs/reference/bag.rst b/docs/reference/bag.rst new file mode 100644 index 00000000..3e01c88c --- /dev/null +++ b/docs/reference/bag.rst @@ -0,0 +1,99 @@ +Bags +==== + +For any :doc:`type ` ``T``, ``Bag(T)`` is the type of *finite +bags* with elements of type ``T``. A bag is like a :doc:`set` (and +unlike a :doc:`list`) in that it doesn't care about the order of the +elements; however, unlike a :doc:`set`, a bag cares *how many copies* +of each element there are. + +* The built-in ``bag`` function can be used to convert other + collections (*e.g.* :doc:`sets ` or :doc:`lists `) to bags. + + :: + + Disco> bag([]) + ⟅⟆ + Disco> bag({1,2,3}) + ⟅1, 2, 3⟆ + Disco> bag("hello") + ⟅'e', 'h', 'l' # 2, 'o'⟆ + +* Notice how single elements are simply listed by themselves, but + elements occuring more than once are written with a ``#`` followed + by a natural number. You can write bags this way yourself: + + :: + + Disco> ⟅'a' # 2, 'b' # 3⟆ + ⟅'a' # 2, 'b' # 3⟆ + Disco> ⟅'a' # 2, 'b' # 1⟆ + ⟅'a' # 2, 'b'⟆ + Disco> ⟅'a' # 0, 'b' # 1⟆ + ⟅'b'⟆ + +* Of course, entering the ``⟅⟆`` characters can be difficult, so you + can also just stick with entering bags via the ``bag`` function. + +* One common place where bags show up is in the output of the ``factor`` + function (from the ``num`` standard library module) for representing + the prime factorization of a natural number. In a prime + factorization, the *order* of the prime factors does not matter (since + multiplication is commutative), but it matters how many copies there + are of each factor. + + :: + + Disco> import num + Disco> factor(10) + ⟅2, 5⟆ + Disco> factor(12) + ⟅2 # 2, 3⟆ + Disco> factor(64) + ⟅2 # 6⟆ + +* Just as with :doc:`lists ` and :doc:`sets `, an + :doc:`ellipsis ` can be used to generate a range of + elements in a bag. For example, + + :: + + Disco> ⟅'a' .. 'e'⟆ + ⟅'a', 'b', 'c', 'd', 'e'⟆ + Disco> ⟅1, 3 .. 9⟆ + ⟅1, 3, 5, 7, 9⟆ + +* :doc:`Comprehension ` notation can also be used, + for example: + + :: + + Disco> ⟅ abs(x - 5) | x in ⟅1 .. 10⟆, x^2 > 5 ⟆ + ⟅0, 1 # 2, 2 # 2, 3, 4, 5⟆ + +* The order of elements in a bag does not matter, but the number of + copies of each element does matter. Two bags with the same elements + in a different order are considered the same, whereas two bags with + the same elements but a different number of copies of each are + considered different. For example, + + :: + + Disco> ⟅1,2,3⟆ == ⟅1,3,2⟆ + T + Disco> ⟅1,2,3⟆ == ⟅1,1,2,3⟆ + F + +* To check whether a bag contains a given element at least once, one can + use the ``elem`` operator (also written ``∈``): + + :: + + Disco> 2 elem ⟅1,2,3⟆ + T + Disco> 5 elem ⟅1,2,3⟆ + F + Disco> 2 ∈ ⟅1,2,3⟆ + T + +XXX operations on bags: intersection, union, power diff --git a/docs/reference/bool.rst b/docs/reference/bool.rst index 6536599c..7bc33307 100644 --- a/docs/reference/bool.rst +++ b/docs/reference/bool.rst @@ -2,8 +2,8 @@ Booleans ======== The type of *booleans* is written ``Bool`` or ``Boolean``. There are -exactly two values of type ``Boolean``: ``false`` and ``true`` (which -can also be written ``False`` and ``True``). +exactly two values of type ``Boolean``: ``F`` and ``T`` (which +can also be written ``False`` and ``True``, or ``false`` and ``true``). :doc:`Logical operators ` can be used to manipulate ``Boolean`` values, and expressions of type ``Boolean`` can be used as diff --git a/docs/reference/compare.rst b/docs/reference/compare.rst index fe5e8d6f..a5567de5 100644 --- a/docs/reference/compare.rst +++ b/docs/reference/compare.rst @@ -15,7 +15,7 @@ can be compared: :: Disco> {(3, "hi"), (4, "there"), (6, "world")} < {(10, "what")} - true + T See the individual pages about each type for more information on how comparison works on values of that type. @@ -36,9 +36,9 @@ many. :: Disco> 3 == 5 - false + F Disco> "hi" == "hi" - true + T Equality is one critical point where Disco syntax has to deviate from standard mathematical notation: be sure to keep in mind the diff --git a/docs/reference/comprehension.rst b/docs/reference/comprehension.rst index 5a90abd1..7c63886b 100644 --- a/docs/reference/comprehension.rst +++ b/docs/reference/comprehension.rst @@ -24,10 +24,10 @@ Examples Disco> {x | x in {1..5}} -- same as {1..5} {1, 2, 3, 4, 5} - + Disco> {3x | x in {1..5}} -- multiply each element of {1..5} by 3 {3, 6, 9, 12, 15} - + -- Pick out the elements of {1..10} that satisfy the condition Disco> {x | x in {1 .. 10}, x^2 + 20 == 9x} {4, 5} @@ -50,7 +50,7 @@ Details Each *qualifier* in a comprehension can be either * a *variable binding* of the form `` in ``, *e.g.* ``x - in {1 .. 10}`` or ``b in {false, true}``, or + in {1 .. 10}`` or ``b in {F, T}``, or * a *guard*, which can be any :doc:`boolean ` expression. A variable binding locally defines a variable and causes it to "loop" through diff --git a/docs/reference/divides.rst b/docs/reference/divides.rst index 19e668ba..c8e9928a 100644 --- a/docs/reference/divides.rst +++ b/docs/reference/divides.rst @@ -9,20 +9,20 @@ example: :: Disco> 3 divides 6 - true + T Disco> 6 divides 3 - false + F Disco> 3 divides (-6) - true + T Disco> 5 divides 5 - true + T Disco> 4 divides 6 - false + F Disco> 0 divides 10 - false + F Disco> 10 divides 0 - true + T Disco> 0 divides 0 - true + T Disco> 1/2 divides 3/2 - true + T diff --git a/docs/reference/expression.rst b/docs/reference/expression.rst index 0e6d1be2..35b1c27c 100644 --- a/docs/reference/expression.rst +++ b/docs/reference/expression.rst @@ -25,5 +25,5 @@ Examples of things which are *not* expressions include: Be careful not to confuse ``x = 3`` (a :doc:`definition ` of the :doc:`variable ` ``x``) with ``x == 3`` (a :doc:`comparison ` expression which has a value of either - ``true`` or ``false`` depending on whether ``x`` is equal to ``3`` or + ``T`` or ``F`` depending on whether ``x`` is equal to ``3`` or not). See :doc:`def-vs-test`. diff --git a/docs/reference/list.rst b/docs/reference/list.rst new file mode 100644 index 00000000..df19597f --- /dev/null +++ b/docs/reference/list.rst @@ -0,0 +1,88 @@ +Lists +===== + +For any :doc:`type ` ``T``, ``List(T)`` is the type of *finite lists* with +elements of type ``T``. A list is an arbitrary *sequence*; that is, a +list is a collection of ``T`` values where the order matters. + +In general, lists are written with square brackets. + +* The empty list is written ``[]``. +* A list with specific elements can be written like this: ``[1, 2, 3]``. +* An :doc:`ellipsis ` can be used to generate a range of + elements. For example, + + :: + + Disco> [1 .. 5] + [1, 2, 3, 4, 5] + Disco> [1, 3 .. 9] + [1, 3, 5, 7, 9] + +* :doc:`List comprehension ` notation can also be used, + for example: + + :: + + Disco> [ abs(x - 5) | x in [1 .. 10], x^2 > 5] + [2, 1, 0, 1, 2, 3, 4, 5] + +* The built-in ``list`` function can be used to convert other + collections (*e.g.* :doc:`sets ` or :doc:`bags `) to lists: + + :: + + Disco> list({1, 2, 3}) + [1, 2, 3] + Disco> import num + Disco> list(factor(12)) + [2, 2, 3] + +* The built-in `append` function can be used to append two lists. + + :: + + Disco> import list + Disco> :type append + append : List(a) × List(a) → List(a) + Disco> append([1,2,3], [5,6]) + [1, 2, 3, 5, 6] + +* Strings (written in double quotes) are really just lists of characters. + + :: + + Disco> |"hello"| + 5 + Disco> append("hello", "world") + "helloworld" + Disco> [(c,1) | c in "hello"] + [('h', 1), ('e', 1), ('l', 1), ('l', 1), ('o', 1)] + +* The order of elements in a list matters. Two lists with elements in a + different order, or different number of copies of the elements, are + not the same. For example, + + :: + + Disco> [1,2,3] == [1,3,2] + F + Disco> [1,2,3] == [1,1,2,3] + F + +* To check whether a list contains a given element, one can use the + ``elem`` operator (also written ``∈``): + + :: + + Disco> 2 elem [1,2,3] + T + Disco> 5 elem [1,2,3] + F + Disco> 2 ∈ [1,2,3] + T + +Inductive definition of lists +----------------------------- + +Write more here. diff --git a/docs/reference/logic-ops.rst b/docs/reference/logic-ops.rst index 8f768725..34463459 100644 --- a/docs/reference/logic-ops.rst +++ b/docs/reference/logic-ops.rst @@ -4,8 +4,8 @@ Logical operations Disco has various standard operations for manipulating :doc:`Boolean values `. -* Logical negation is written ``not``; it inverts ``true`` to - ``false`` and vice versa. +* Logical negation is written ``not``; it inverts ``T`` to + ``F`` and vice versa. * Logical conjunction, aka AND, is written ``/\``, ``and``, or ``&&``. It has the following truth table: diff --git a/docs/reference/prop.rst b/docs/reference/prop.rst index 0ede6f68..a18700a3 100644 --- a/docs/reference/prop.rst +++ b/docs/reference/prop.rst @@ -4,12 +4,12 @@ Propositions ``Prop`` is the type of *propositions*. A proposition is a statement that could be true or false. ``Prop`` is very similar to ``Bool``; the main difference is that whereas any ``Bool`` can always be -evaluated to see if it is ``true`` or ``false``, this may not be +evaluated to see if it is ``T`` or ``F``, this may not be possible for a ``Prop`` due to the use of quantifiers (``forall`` and ``exists``). Any :doc:`Boolean ` expression can be used as a proposition. -For example, ``true``, ``x > 5``, and ``(x < y) -> ((x == 2) \/ (x == +For example, ``T``, ``x > 5``, and ``(x < y) -> ((x == 2) \/ (x == 3))`` can all be used as propositions. However, unlike Boolean expressions, propositions can use :doc:`quantifiers @@ -23,12 +23,12 @@ whether a proposition is true or false, you have two options: - The built-in ``holds`` function tries its best to determine whether a proposition is true or false. If it returns a value at all, it is definitely correct. For example, - - ``holds ((5 < 3) \/ ((2 < 1) -> false))`` yields ``true`` + - ``holds ((5 < 3) \/ ((2 < 1) -> F))`` yields ``T`` - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (q \/ p))`` - yields ``true`` + yields ``T`` - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q))`` - yields ``false`` - - ``holds (forall n:N. n < 529)`` yields ``false`` + yields ``F`` + - ``holds (forall n:N. n < 529)`` yields ``F`` However, sometimes it may simply get stuck in an infinite loop. For example, ``holds (forall n:N. n >= 0)`` will simply get stuck. Even though it is obvious to us that this proposition is true, ``holds`` @@ -38,7 +38,7 @@ whether a proposition is true or false, you have two options: - One can also use the ``:test`` command. This command makes a best effort to evaluate a proposition, but only trying a finite number of examples for infinite domains. Additionally, in many cases it can - output much more information than a simple ``true`` or ``false``, + output much more information than a simple ``T`` or ``F``, for example, showing a counterexample if a ``forall`` is false, or a witness if an ``exists`` is true. For example, - ``:test forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q)`` @@ -48,8 +48,8 @@ whether a proposition is true or false, you have two options: - Certainly false: ∀p. ∀q. p \/ q <-> p /\ q Counterexample: - p = false - q = true + p = F + q = T - However, ``:test forall n:N. n < 529`` prints diff --git a/docs/reference/set-ops.rst b/docs/reference/set-ops.rst index 28c0425f..d65f2c20 100644 --- a/docs/reference/set-ops.rst +++ b/docs/reference/set-ops.rst @@ -34,9 +34,9 @@ You can check whether one set is a subset of another using the :: Disco> {2,3,4} subset {1 .. 10} - true + T Disco> {7 .. 11} subset {1 .. 10} - false + F Note that Disco does not support the set complement operation, since the complement of a finite set is infinite whenever the domain is diff --git a/docs/reference/set.rst b/docs/reference/set.rst index 953c265c..e34a5ba0 100644 --- a/docs/reference/set.rst +++ b/docs/reference/set.rst @@ -49,11 +49,11 @@ To check whether a set contains a given element, one can use the :: Disco> 2 elem {1,2,3} - true + T Disco> 5 elem {1,2,3} - false + F Disco> 2 ∈ {1,2,3} - true + T Sets support various operations, including :doc:`size `, :doc:`union `, :doc:`intersection `, diff --git a/docs/reference/sum-type.rst b/docs/reference/sum-type.rst index 480c6103..80a98a7d 100644 --- a/docs/reference/sum-type.rst +++ b/docs/reference/sum-type.rst @@ -18,8 +18,8 @@ Sum types Disco> left(3) : N + Bool left(3) - Disco> right(false) : N + Bool - right(false) + Disco> right(F) : N + Bool + right(F) Note that the ``left`` or ``right`` ensures that ``A + B`` really does represent a *disjoint* union. For example, although the usual