diff --git a/docs/and.rst b/docs/and.rst new file mode 100644 index 0000000..aa7b1f9 --- /dev/null +++ b/docs/and.rst @@ -0,0 +1,57 @@ +and +=== + +The built-in function ``and`` accepts one or more :ref:`sentence expression values ` and returns a sentence which links each argument sentence using the ``&`` :ref:`connective `. + +Syntax +------ + +.. code-block:: + + and([sentence argument expression], ...) + +Behavior +-------- + +``and`` accepts one or more argument expressions. If any argument expression does not evaluate to a :ref:`sentence expression value ` or any argument sentence has unbound objects or predicates, then an error is raised. Otherwise, the output is a sentence composed of each argument sentence joined in order using the ``&`` :ref:`connective `. + +The output sentence value is verified if every argument sentence value is verified. + +Examples +-------- + +If ``in`` is a :doc:`relation `, ``arg0`` stores the verified sentence: + +.. code-block:: + + *X*Y(~X in Y | ~Y in X) + +And ``arg1`` stores the verified sentence: + +.. code-block:: + + ~^X(X in X) + +Then the following expression: + +.. code-block:: + + and(arg0, arg1) + +Evaluates to the following verified sentence: + +.. code-block:: + + *X*Y(~X in Y | ~Y in X) & ~^X(X in X) + +Additionally, the following expression: + +.. code-block:: + + and(arg0, <:^X^Y(X in Y & Y in X)>, <:^E*X(~X in E)>) + +Evaluates to the following unverified sentence: + +.. code-block:: + + *X*Y(~X in Y | Y in X) & ^X^Y(X in Y & Y in X) & ^E*X(~X in E) diff --git a/docs/builtin.rst b/docs/builtin.rst new file mode 100644 index 0000000..310fe45 --- /dev/null +++ b/docs/builtin.rst @@ -0,0 +1,13 @@ +Built-in Functions +================== + +There are a few built-in functions for manipulating :ref:`expression values ` in CORE. Each built-in function expression begins with an identifier followed by a ``(`` character. A built-in function expression term evaluates to the output of the function. You can determine the behavior of the built-in functions in the documents below. + +.. toctree:: + :titlesonly: + + left + right + and + or + diff --git a/docs/connectives.rst b/docs/connectives.rst index e4f1dc2..a8a06ba 100644 --- a/docs/connectives.rst +++ b/docs/connectives.rst @@ -28,6 +28,8 @@ The logical connective ``&`` represents "and." If ``{A}`` and ``{B}`` represent Sentences composed with the ``&`` logical connective can be constructed using the built-in function :doc:`and `. A sentence composed with the ``&`` connective can be deconstructed into its constituent sentences using :doc:`variable assignment `. A sentence ``{C}`` is stronger than the sentence ``{A} & {B}`` if ``{C}`` is stronger than both ``{A}`` and ``{B}``. The sentence ``{A} & {B}`` is stronger than a sentence ``{C}`` if either ``{A}`` or ``{B}`` is stonger than ``{C}``. See :ref:`Trivial Implication ` for more information. +.. _or: + Or --- diff --git a/docs/expressions.rst b/docs/expressions.rst index fd53050..b85e246 100644 --- a/docs/expressions.rst +++ b/docs/expressions.rst @@ -13,6 +13,7 @@ Expressions allow the programmer to combine expression values to obtain new expr Deduction Sentence Constants Expression Brackets + Built-in Functions .. _`expressionvalues`: diff --git a/docs/left.rst b/docs/left.rst new file mode 100644 index 0000000..c367202 --- /dev/null +++ b/docs/left.rst @@ -0,0 +1,61 @@ +left +==== + +The built-in function ``left`` accepts one :ref:`sentence expression value ` and returns the left-hand side of the sentence. It's precise behavior depends on the input value. + +Syntax +------ + +.. code-block:: + + left([sentence argument expression]) + +Behavior +-------- + +If the argument does not evaluate to a sentence expression value or the argument sentence has unbound objects or propositions, an error is raised. + +The following lists the behavior of the function depending on the argument sentence type: + +- If the argument sentence is of the form ``A & B``, then the output is the sentence ``A``. The output is verified if and only if the argument sentence is verified. +- If the argument sentence is of the form ``A | B``, then the output is the sentence ``A``. The output is unverified. +- If the argument sentence is of the form ``A -> B``, then the output is the sentence ``A``. The output is unverified. +- If the argument sentence is of the form ``A <-> B``, then the output is the sentence ``B -> A``. The output is verified if and only if the argument sentence is verified. +- If the argument sentence is not any of these types, an error is raised + +.. note:: + Since this function's output depends on the association of the operations composing the argument sentence which normally doesn't matter, this function's use is not recommended. Oftentimes this function's purpose is overshadowed by :ref:`trivial implication ` and :doc:`variable assignment `. + +Examples +-------- + +If ``X`` and ``Y`` are objects, ``<`` is a relation, the output of the following expression: + +.. code-block:: + + left(<: X < Y & Y < X>) + +Is the unverified sentence: + +.. code-block:: + + X < Y + +If ``X`` is an object, ``empty`` is a :doc:`definition `, ``in`` is a :doc:`relation `, and ``test`` stores the verified sentence: + +.. code-block:: + + ^E(empty(E) & E in X) & ~X in X + +Then the output of the following expression: + +.. code-block:: + + left(test) + +Is the verified sentence: + +.. code-block:: + + ^E(empty(E) & E in X) + diff --git a/docs/or.rst b/docs/or.rst new file mode 100644 index 0000000..f0e583a --- /dev/null +++ b/docs/or.rst @@ -0,0 +1,57 @@ +or +=== + +The built-in function ``or`` accepts one or more :ref:`sentence expression values ` and returns a sentence which links each argument sentence using the ``|`` :ref:`connective `. + +Syntax +------ + +.. code-block:: + + or([sentence argument expression], ...) + +Behavior +-------- + +``or`` accepts one or more argument expressions. If any argument expression does not evaluate to a :ref:`sentence expression value ` or any argument sentence has unbound objects or predicates, then an error is raised. Otherwise, the output is a sentence composed of each argument sentence joined in order using the ``|`` :ref:`connective `. + +The output sentence value is verified if at least one argument sentence value is verified. + +Examples +-------- + +If ``in`` is a :doc:`relation `, ``arg0`` stores the verified sentence: + +.. code-block:: + + *X*Y(~X in Y | ~Y in X) + +And ``arg1`` stores the verified sentence: + +.. code-block:: + + ~^X(X in X) + +Then the following expression: + +.. code-block:: + + or(arg0, arg1) + +Evaluates to the following verified sentence: + +.. code-block:: + + *X*Y(~X in Y | ~Y in X) | ~^X(X in X) + +Additionally, the following expression: + +.. code-block:: + + or(arg0, <:^X^Y(X in Y & Y in X)>, <:^E*X(~X in E)>) + +Evaluates to the following verified sentence: + +.. code-block:: + + *X*Y(~X in Y | Y in X) | ^X^Y(X in Y & Y in X) | ^E*X(~X in E) diff --git a/docs/right.rst b/docs/right.rst new file mode 100644 index 0000000..6a5aced --- /dev/null +++ b/docs/right.rst @@ -0,0 +1,61 @@ +right +===== + +The built-in function ``right`` accepts one :ref:`sentence expression value ` and returns the right-hand side of the sentence. It's precise behavior depends on the input value. + +Syntax +------ + +.. code-block:: + + right([sentence argument expression]) + +Behavior +-------- + +If the argument does not evaluate to a sentence expression value or the argument sentence has unbound objects or propositions, an error is raised. + +The following lists the behavior of the function depending on the argument sentence type: + +- If the argument sentence is of the form ``A & B``, then the output is the sentence ``B``. The output is verified if and only if the argument sentence is verified. +- If the argument sentence is of the form ``A | B``, then the output is the sentence ``B``. The output is unverified. +- If the argument sentence is of the form ``A -> B``, then the output is the sentence ``B``. The output is unverified. +- If the argument sentence is of the form ``A <-> B``, then the output is the sentence ``A -> B``. The output is verified if and only if the argument sentence is verified. +- If the argument sentence is not any of these types, an error is raised + +.. note:: + Since this function's output depends on the association of the operations composing the argument sentence which normally doesn't matter, this function's use is not recommended. Oftentimes this function's purpose is overshadowed by :ref:`trivial implication ` and :doc:`variable assignment `. + +Examples +-------- + +If ``X`` and ``Y`` are objects, ``<`` is a relation, the output of the following expression: + +.. code-block:: + + right(<: X < Y & Y < X>) + +Is the unverified sentence: + +.. code-block:: + + Y < X + +If ``X`` is an object, ``empty`` is a :doc:`definition `, ``in`` is a :doc:`relation `, and ``test`` stores the verified sentence: + +.. code-block:: + + ^E(empty(E) & E in X) & ~X in X + +Then the output of the following expression: + +.. code-block:: + + right(test) + +Is the verified sentence: + +.. code-block:: + + ~X in X +