diff options
Diffstat (limited to 'docs/semantics.rst')
| -rw-r--r-- | docs/semantics.rst | 441 |
1 files changed, 441 insertions, 0 deletions
diff --git a/docs/semantics.rst b/docs/semantics.rst new file mode 100644 index 0000000..9cc19a1 --- /dev/null +++ b/docs/semantics.rst @@ -0,0 +1,441 @@ +.. _semantics: + +######### +Semantics +######### + +.. highlight:: scheme + +Forms are also the most basic unit of Actinide evaluation. Execution of an +Actinide program proceeds by *reducing* one form to a simpler result, until +only a single irreducible form is left (which is the program's result). + +Most Actinide programs consist of a top-level compound form, which must be +fully reduced to run the program to completion. The following sections describe +the mechanism and results of reducing each kind of form. In general, evaluation +proceeds by reducing the inner-most, left-most unreduced form, iteratively, +until all forms have been reduced. + +******** +Literals +******** + +Literal forms reduce to themselves, unchanged. The following forms are +considered literal forms: + +* Integers +* Decmials +* Strings +* Booleans + +For example, the result of reducing ``1`` is ``1``. + +******* +Symbols +******* + +Symbols, other than those that are part of :ref:`special forms <special +forms>`, represent variables in Actinide programs, and reduce to the values of +those variables in the current *environment*. + +In an environment where a symbol has a value, the reduction of that symbol is +the value it's bound to. In an environment where a symbol is not bound to any +value, the reduction of that symbol produces an error and stops the computation. + +For example, in an environmet where the symbol ``x`` is bound to ``5``, the +result of reducing ``x`` is ``5``. + +An Actinide program is run in an initial *top-level environment*, which comes +pre-populated with bindings for all of Actinide's built-in functions and +values, plus any values placed there by the host program. As Actinide reduces a +program, the bindings in that initial environment can change, and additional +environments may be created. The *current environment* is controlled by the +:ref:`lambda` form and by :ref:`procedure application`. + +.. _special forms: + +************* +Special forms +************* + +Lists that begin with one of the following symbols are evaluated specially. + +~~~~~ +quote +~~~~~ + +Syntax: + +.. code-block:: scheme + + (quote form) + +A ``quote`` form guards another form from evaluation. The result of reducing a +quote form is exactly the guarded ``form``. This allows forms that may have +special meaning, such as lists, to be embedded in Actinide programs as literal +values, stripped of their special meaning. + +.. _begin: + +~~~~~ +begin +~~~~~ + +Syntax: + +.. code-block:: scheme + + (begin [form-1 ... form-n]) + +A ``begin`` form fully evaluates each subform in left-to-right order, then +reduces to the value of the final subform. This allows for forms with side +effects to be evaluated (and their results ignored) before evaluating a final +form that produces a result. + +An empty ``begin`` form evaluates to the empty list. + +Example: + +.. code-block:: scheme + + (begin + ; define a function... + (define (f) 1) + ; ...and call it + (f)) + +.. _if: + +~~ +if +~~ + +Syntax: + +.. code-block:: scheme + + (if cond if-true) + (if cond if-true if-false) + +An ``if`` form conditionally evaluates one of two forms based on the result of +a condition. The ``cond`` form is fully evaluated first; if it reduces to a +true value, then the ``if-true`` form is evaluated and the ``if`` form reduces +to its result; otherwise, the ``if-false`` form is evaluated and the ``if`` +form reduces to its result. In either case, the other form is discared without +evaluation. + +An ``if`` form without an ``if-false`` form reduces to nil if the ``cond`` form reduces to a false value. + +The following values are false: + +* the empty list +* ``#f`` +* integer and decimal zeroes +* empty strings +* empty vectors + +All other values are true. + +Example: + +.. code-block:: scheme + + (if #t 'was-true 'was-false) + + (if (goldback-conjecture) + "Eureka!") + +.. _lambda: + +~~~~~~ +lambda +~~~~~~ + +Syntax: + +.. code-block:: scheme + + (lambda formals [body-1...body-n]) + +Defines a procedure taking arguments described by the ``formals`` form, whose +application will evaluate the ``body`` forms in order and will reduce to the +result of the last form. + +The ``formals`` form must have one of the following structures: + +* A list of symbols, each of which will be bound to a single argument when the + procedure is applied, in the order listed. + +* An improper list of symbols. Each symbol other than the final tail symbol + will be bound to an argument from the procedure application; the final tail + symbol will be bound to a list of all arguments that were not bound to any + other symbol. + +* A single symbol, which will be bound to a list of the arguments when the + procedure is applied. + +A ``lambda`` form reduces to a newly-created procedure value whose body is the +list of body forms and whose formal argument list is the formals. + +Each procedure captures the environment in effect when the ``lambda`` form is +evaluated, allowing the procedure body to see variables that were visible at +that time, even if the procedure outlives the context where that environment is +defined. + +Each time a procedure is applied, Actinide creates a new environment that +inherits from the captured environment and binds the values of arguments from +the procedure application to the symbols named in the procedure's ``formals``. +This is the primary mechanism for creating new environments in Actinide. +Procedure application then evaluates the body forms, in that new environment, +in left-to-right order. The result of the final form is the result of the +procedure application. (In fact, procedures whose bodies consist of multiple +forms, or of no forms at all, are converted to a procedure whose body is a +single ``begin`` form.) + +Examples: + +.. code-block:: scheme + + ; Creates a constant function of zero arguments, which always + ; evaluates to 1. + (lambda () 1) + + ; Defines a variable in the current environment (as discussed + ; below), then creates a function of zero arguments that returns + ; that variable. Initially, it will always return 5, but if the + ; value of x is changed in the outer environment, the function's + ; return value will change as well. + (begin + (define x 5) + (lambda () x)) + + ; Defines a function of two arguments, a and b, whose result is + ; the sum of those arguments. This is a simple alias for the + + ; built-in function, illustrating the idea that functions can + ; call other functions. + (lambda (a b) (+ a b)) + + ; Defines a function that takes one or more arguments, with the + ; first argument bound to a (and ignored) and the list of + ; remaining arguments bound to b. This always returns b + ; unchanged, and throws away a. + (lambda (a . b) b) + + ; Defines a function that takes any number of arguments, and + ; returns them as a list. This is a simple alias for the list + ; built-in function. + (lambda a a) + +.. _define: + +~~~~~~ +define +~~~~~~ + +Syntax: + +.. code-block:: scheme + + (define symb form) + (define signature [body-1...body-n]) + +A define form creates a new variable in the current environment, and binds a +value to that variable. There are two variations on this form: simple +definition and procedure definition. + +In the first form, the ``symb`` subform must be a single symbol. The ``form`` +subform is fully reduced, and the resulting value is bound to the variable +``symb`` in the current environment. For example: + +.. code-block:: scheme + + (begin + ; Defines a variable, x, whose initial value is 5. + (define x 5) + ; Evaluates to the value of x. + x) + +In the second, the ``signature`` subform must be a procedure signature: a list +or improper list of symbols. The first element of that list is the name the +procedure will be bound to, while the rest of that list is treated as the +``formals`` form as described under :ref:`lambda`. The list of ``body`` forms become +the resulting procedure's body, as usual. + +Under the hood, the second form is translated into the first automatically - +the form + +.. code-block:: scheme + + (define (sum a b) (+ a b)) + +is exactly equivalent to the form + +.. code-block:: scheme + + (define sum + (lambda (a b) (+ a b))) + +However, when the option is available, procedure definition should be preferred +as it's generally more readable. + +~~~~~~ +values +~~~~~~ + +Syntax: + +.. code-block:: scheme + + (values [body-1...body-n]) + +Where most forms reduce to a single value, the ``values`` form reduces to a +sequence of values, in place. This allows a function or any other form to +reduce to multiple distinct values, which can be inserted into other forms. + +The body forms are evaluated left-to-right, and the ``values`` form reduces to +the resulting values, left-to-right. + +Example: + +.. code-block:: scheme + + (begin + ; A function which returns two values, both equal to its + ; sole argument + (define (two x) (values x x)) + ; = accepts two values and compares them. + (= (two 53))) + +.. _define-macro: + +~~~~~~~~~~~~ +define-macro +~~~~~~~~~~~~ + +Syntax: + +.. code-block:: scheme + + (define-macro symb form) + (define-macro signature [body-1...body-n]) + +A ``define-macro`` form creates a new :ref:`macro transformer <macros>` +function in the current environment's macro table. This is identical to the +:ref:`define` form, but the resulting binding is not visible as a variable, and +affects macro expansion of Actinide programs. Macro bindings using the first +form must bind the symbol to a procedure or built-in function producing exactly +one result. + +.. warning:: + + A ``define-macro`` form which appears within a procedure body will create a + macro in the environment created when the procedure is applied. These + macros are **never** visible to the macro expander, and will have no effect. + +.. _procedure application: + +********************* +Procedure application +********************* + +Any list which is not empty, and not a :ref:`special form <special forms>`, is +a procedure application, applying either a built-in procedure (provided by +Actinide or by the host program) or a procedure defined using the :ref:`lambda` +special form or any of its :ref:`equivalents <define>`. + +Syntax: + +.. code-block:: scheme + + (fn [arg-1...arg-n]) + +The subforms of a list form are evaluated from left to right. The ``fn`` +subform must evaluate to a procedure; the remaining ``body`` forms are +evaluated to produce the values of arguments to that procedure. Once all of the +subforms have been evaluated, the procedure is applied to its arguments, and +the procedure application itself reduces to the result of the applied procedure. + +During the application of a procedure, + +1. A new *child* environment is created from the procedure's captured + environment. In this environment, any name not defined in the child + environment is looked up in the captured environment instead. + +2. The values of the arguments from the function application form are bound to + the names given by the procedure's formal arguments list. + +3. The procedure's body forms are evaluated from left to right in the child + environment. + +4. The result of the last form in the procedure body is used as the result of + the function application. + +~~~~~~~~~~~~~~~~~~~ +Loops and Recursion +~~~~~~~~~~~~~~~~~~~ + +Actinide has no primitives dedicated to repeating parts of a program. To loop, +a procedure must recurse. Actinide guarantees that recursion in *tail position* +can proceed arbitrarily far without exhausting any resources solely due to the +number of recursive calls. Actinide guarantees tail recursion. + +The following forms are considered to be in tail position: + +* The final form of a :ref:`procedure body <lambda>` is in tail position with + respect to the application of that procedure. + +* The final form of a :ref:`begin` form is in tail position with respect to the + ``begin`` form itself. + +* The ``if-true`` form of an :ref:`if` form whose condition is true, and the + ``if-false`` form of an ``if`` form whose condition is not true, is in tail + position with respect to the ``if`` form. + +* If a form is in tail position with respect to another form, it is also in + tail position for any form that form is in the tail position of, and so on + outwards until the form is either in tail position with respect to the root + of the program or a form is found for which the containing form is not in + tail position. + +As an example, the following implementation of the factorial algorithm is +recursive, but the recursion does not appear in tail position (it is not *tail +recursive*): + +.. code-block:: scheme + + (define (factorial n) + (if (= n 1) + 1 + (* n (factorial (- n 1))))) + +The ``factorial`` function *is not* called in tail position with respect to the +body of the ``factorial`` function: After reducing the inner application of +``factorial``, the reduction of the outer ``factorial`` application must +continue so that it can apply the ``*`` function to the result. + +Attempting to evaluate ``(factorial 1000)`` fails due to limits on call depth: +``maximum recursion depth exceeded while calling a Python object`` + +.. note:: + + This warning leaks some implementation details, obviously. The exact + failure mode should not be relied on; the key property is that + deeply-recursive programs will raise an error when they exhaust the + implementation's resources. + +The following implementation of the factorial algorithm *is* tail-recursive: + +.. code-block:: scheme + + (define (fact n a) + (if (= n 1) + a + (fact (- n 1) (* n a)))) + +The ``fact`` function is called in tail position with respect to the body of +``fact``. Specifically, it is in tail position with respect to the ``if`` form +whenever ``n`` is not equal to ``1``, and the ``if`` form is in tail position +with respect to the body of the ``fact`` function. + +Evaluating ``(fact 1000 1)`` correctly computes the factorial of ``1000`` on +any machine with enough memory to store the result. |