------------------------------------------------------------------------
[LAMBDA.MAN].ATARI.ST [1.37][890304], revised from MAC.LS [1.28][890116]
------------------------------------------------------------------------

  LAMBDA : A LAMBDA-CALCULUS INTERPRETER AND COMBINATORY CODE GENERATOR

                            Adrian Rezus (1989)
             
   0. LAMBDA is a lazy micro-interpreter for [type-free] LAMBDA-calculus 
   [BETA-] reductions and standard combinator expansions [i.e., the Curry 
   "abstraction algorithms"]. The evaluator does "standard" [left-to-right, 
   left-most-outermost] reductions, using an idea of W. L. van der Poel 
   [formerly at the Technological University of Delft, The Netherlands]. 
   It runs in different variants, on almost any machine for which a 
   reasonable C-compiler is available. BCPL and [Franz, Mu, etc.] LISP 
   variants are also operational. LAMBDA includes also an ASCII-editor, 
   based on Ken Thompson's `ed' [the "standard" UN*X editor], intended 
   for use in LAMBDA-input preparation. If a UN*X-like shell is present, 
   LAMBDA acts as an extension of the current shell. 

   0.0 COPYRIGHT SPECIFICATIONS:

       This program has no specific restrictions as regards duplication
       and/or modification, as far as the this re-distribution does not 
       have commercial purposes. Also, no "share-" [and/or any other 
       kind of] "...-ware" use-restrictions are applicable.      
 
       On the other hand, no "user-" and/or "upgrade-support" can be
       provided, otherwise than by private mail and/or - if necessary 
       - via the appropriate [...NET].NEWS-channels.

       Portions of the code incorporated in the current version of 
       LAMBDA are based on copyrighted material and/or some - otherwise
       excellent - public domain software packages [C-libraries, etc.]. 
       The exact references to this kind of material are specified in 
       the source-code, for each particular machine/environment. The 
       source-code cannot be re-distributed and/or circulated "as is" 
       without these acknowledgements. 

       The binaries - originally provided - should also contain, as an 
       internal "stamp", such acknowledements, either user-transparent 
       [via a built-in command `version'] or user-hidden by a static 
       declaration and/or by other means. The actual contents of such 
       a "stamp" should mainly depend on the compiler options used to 
       generate the current version of LAMBDA. The binaries cannot be
       re-distributed and/or circulated without this internal "stamp".

   0.1 BASIC REFERENCES [type-free lambda-calculus and combinators]:
   
     J. R. HINDLEY, J. P. SELDIN "Introduction to Combinators and 
        Lambda-calculus", Cambridge UP: London etc. 1986 [London
        Mathematical Society Student Texts 1]. [Up-to-date upgrade
        of the first - 1972 - elementary introduction to lambda-
        calculus. Main audience: students in mathematics and computer 
        science. Highly readable, even by non-experts. The authors 
        are - both - former students of H. B. Curry, the father - 
        one of them, anyway - of combinatory "logic".]
     R. M. SMULLYAN "To Mock a Mocking-Bird", Knopf: New York, 1985.
        [An ingenious ornithological metaphor around combinator-
        behaviors. Offers a pleasant - non-mathematical - access to 
        the world of lambda/combinators. Read this first if you have
        never heard about combinators or lambda-calculus before!]
     H. P. BARENDREGT "The Lambda Calculus, Its Syntax and Semantics",   
        North Holland: Amsterdam etc. 1981. [The basic treatise. Main
        audience: mathematics/computer science students and researchers
        in theoretical computer science. Second revised edition: 1984.]
     A. REZUS "A Bibliography of Lambda-calculi, Combinatory Logics 
        and Related Topics", Mathematical Centre: Amsterdam 1982.
        [Currently distributed by: CWI, Kruislaan 413, Amsterdam, NL.]
     A. REZUS "On a singleton basis for the set of closed lambda-terms",
        Libertas mathematica (Arlington TX) 2, 1982, page 94. [Documents
        Carew Meredith's (shortest) generator; i. e.  MU, sub 1 below.]
     A. REZUS "Lambda-conversion and Logic", Ph. D. Diss., Utrecht 1981.
        [Monograph of a modern version of Church's original calculus of
        lambda-conversion, as improved within his school - S. C. Kleene, 
        J. B. Rosser and A. Turing - during the early thirthies; the 
        advanced parts contain applications to logic and arithmetic.]
     W. L. VAN DER POEL et al. "New arithmetical operators in the theory 
        of combinators", Indagationes mathematicae 42, 1980, pp. 271-325.
        [The main idea of the present implementation. Contains also the 
        stripped-down source of a LISP-variant, due to G. van der Mey.]
     C. BOEHM, W. GROSS "Introduction to the CUCH", in: E. R. CAIANIELLO
        (editor) "Automata Theory", Academic Press: New York etc., 1966, 
        pp. 35-65. [Apparenty, CUCH (short for "CURRY + CHURCH") is the 
        first implementation of lambda-calculus, at least in Europe.]
     H. B. CURRY et al. "Combinatory Logic" (2 vols.), North Holland: 
        Amsterdam, 1958, 1972. [The old encyclopaedia. Reprinted since.]
     A. CHURCH "The Calculi of Lambda-Conversion", Princeton University 
        Press, Princeton 1941. [The first book on the subject, derived 
        from a Princeton logic course (1935-1936) of the author. Second 
        edition: 1951; also University Microfilms: Ann Arbor reprints.]

   0.3  OTHER REFERENCES:

     B. W. KERNIGHAN & R. PIKE "The UN*X Programming Environment",
        Prentice Hall International Inc. London 1984 [Prentice Hall 
        Software Series]. [Useful mainly for the discussion of the 
        editor, the pattern matching utilities and the "standard" 
        shell environment/support.]

   0.3  VERSION [ver$]:

        current:    'lambda 1.37a [ATARI.ST][UN*X BSD][MINIX].C'
                    'lambda 1.30m [Apple MACintosh].[MFS].C'

        prototypes: 'mlambda.2.1.ATARI.ST.[Mark Williams].C', 
                    'mlambda.2.0.BSD.C',
                    'lambda.1.1.MAC.[Lightspeed].C'

   0.31 HISTORY OF CODE: 

        This version is a conversion from BCPL [Richards standard] 
           version [lambda.4.0.REZUS.BCPL:KU.NIJMEGEN]. 

        Ancestors [LIFO-order]: 
           version [lambda.4.30.REZUS.BSD.C:KU.NIJMEGEN], 
           version [comb.1.0.NIJENHUIS.EXIDY.BDS.C:TU.DELFT], 
           version [comb.[antique].VAN-DER-MEY.PDP11.LISP:TU.DELFT], 
           version [comb.[Ur-version].VAN-DER-MEY.PDP11.ALIAS:TU.DELFT].

        Dutch cousins [best known to me]:
           version [lambda.l.REZUS.BSD.[+ FRANZ:Opus.38.69].LISP:KU.NIJMEGEN],
           version [Lambda-&-Combinators.NIJENHUIS.MSDOS.LATTICE.C:TU.DELFT],
           version [lc.KOYMANS.VMS.ALGOL68:RU.UTRECHT] [advanced, lost!].
 
   0.32 COMPILERS [for tested variants of `lambda': current version]:

     - [UN*X BSD]:   the "portable C compiler" and/or derivatives

     - [MINIX]:      MINIX-ST C, ACK 

     - [ATARI.ST]:   MARK WILLIAMS C 3.06, 
                     LATTICE C 3.04.01 
                     TURBO C [for PROTO-typed variant of MW C version] 

     - [MAC]:        LIGHTSPEED C [> 2.02] 

   0.4 NOTICE ON [WARNING(S)]: Supposedly dangerous actions in `lambda' 
       are marked with an "!" appearing below on the left hand side of 
       a [WARNING] or of a technical note [NB]!   
   !   Example: [WARNING]: See 2.0.A1!

   0.5 DOCUMENTATION: This document specifies briefly only the global
       features of `lambda' and is not intended to describe in detail 
       any particular implementation. The general pattern is UN*X-like, 
       however. Idiosyncrasies, diverging from this usage on a SPECIFIC 
       machine/operating-system, more information, specific problems, 
       etc. are contained in the following documents: 
       
         (description: [audience]: <title-of-document> <comments>).

       - [programmers]: 
         "LAMBDA Source-Code" [actual size is system-specific: 115-165 Kb].

       - [other]: 
         "LAMBDA.[VERSION].[MACHINE].[LANGUAGE].[COMPILER] Technical Notes",
         NB: Some "LAMBDA [...] Technical Notes" may NOT be available.
                   
       - [general]: 
         "A LAMBDA-Tutorial" [in preparation].
 
       - [general, lambda-calculus hackers]: 
         "A History of Lambda-calculus/Combinator Interpreters" [draft].
  
       - [general]: Sample input shell-scripts.

       - [general]: Sample term-libraries. 

   1. SYNTAX. The MAIN [INTERPRETER-] module of `lambda' recognizes the 
      following TERM-SYNTAX:

       NB: Greek `LAMBDA' prints as `L' in the current C-version and below.

       NB: Below, `print-name' refers to the portable, ASCII-only variant.

       - BUILT-IN ATOMS: <name> [<print-name>] = <semantics>
   !     NB: These are reserved symbols in default mode. The user may 
   !         re-define the reserved symbols with the appropriate 
   !         evaluation option ["mode"]. Caution!

         mode [lib-]:
         NB: Minimal set: active in [lc]-, [cl]-, [cl conv]-modes.
       
          #   [#]    =  an arbitrary atom [not user definable!], 
                        [used as an internal dummy or as a head-variable]
          S   [S]    =  (Lx(Ly(Lz(xz(yz)))))
          K   [K]    =  (Lx(Lyx)) 
          I   [I]    =  (Lxx)
          B   [B]    =  (Lx(Ly(Lz(x(yz))))) 
          C   [C]    =  (Lx(Ly(Lz(xzy))))
          W   [W]    =  (Lx(Ly(xyy)))
          ()  [none] =  NIL 
                        [vanishes, behaving as (I) - IF in head-position 
                         evaluates to the dummy #  - ELSE]

         mode [lib+]:
         NB: Activates the following atomic [lc]-behaviors 
             (re-activating the minimal set above, if necessary).
   !     NB: Mode [lib+] restores the behavior of all reserved symbols
   !         (i. e., erases user definitions of built-ins, if any).
   !     NB: SUCC, SUM, PROD, EXP have the expected behavior only on 
   !         Church numerals: <0> = (KI), <n+1> = (SUCC <n>)
 
          #    [#] =  an arbitrary atom           [user definable dummy]
          J    [J] =  (Lx(Ly(Lz(Lu(xu(xyz))))))   [Rosser's J]
          PHI  [F] =  (Lx(Ly(Lz(Lu(x(yu(zu))))))) [Curry's PHI]
          PSI  [U] =  (Lx(Ly(Lz(Lu(x(yz(yu))))))) [Curry's PSI]
          PI   [P] =  (Lx(Ly(Lz(z(xy)))))         [Church's PAIRing]
          ZERO [0] =  (Lx(Lyy))                   [Church's NULL-numeral]
          SUCC [$] =  (Lx(Ly(Lz(y(xyz)))))        [Church's SUCCessor]
          SUM  [+] =  (Lx(Ly(Lz(Lu(xz(yzu))))))   [Rosser SUM]
          PROD [B] =  (Lx(Ly(Lz(x(yz)))))         [Rosser PRODuct]
          EXP  [^] =  (Lx(Ly(yx)))                [Rosser EXPonentiation]
          MU   [M] =  (Lx(Ly(Lz(y(Luz)(xz)))))    [Carew Meredith's generator]

       - LAMBDA-syntax [a, b are terms]:
         ( <atom> ),              - <atom> is a single symbol
         ( a b )
         ( Lx (a) )

         Examples: (Lx(Lyy)), (Lx(Ly(Lz(y(Luz)(xz))))), ...
  
       - COMBINATOR-syntax [a, b are terms]:
         ( <atom> )               - built-in on start: S K I B C W  
         ( a b )

         Examples: (SI), (BC(KI)), (BK), (SKK), (WWW), ...

       - LISP-like syntax [a is a term, defined is a <(head-)list>]:
          ()                      - NIL
          ( a <list> )

          Examples ["==>" means "evaluates to the value of"]:
            ( (BC) (BI) (CK) )         ==> (#(BC)(BI)(CK))
            ( (BI) ( (BC) () ) )       ==> (#(BI)(#BC))

       NB: NO SPACEs in a <term>, except in head-position. 
          Examples [see also the section on PRE-PROCESSING]:  
            (Lx (Ly (x y) ) )          ==> (Lx(Ly(xy)))
            (B( B   I S)C K)           ==> (B(BIS)CK)
            ( (B I)( (B C  ) (  ) ) )  ==> (#(BI)(#BC))

       NB: User-input is PRE-PROCESSED with automatic error recovery.
       NB: LAMBDA-, COMBINATOR- and LIST-syntax can be mixed, as in CUCH.

   2. THE [MAIN] COMMAND INTERPRETER. 
   !   NB [WARNING]: Some commands may be different in other versions.
   
   2.0. EXECUTING 'MODES'.

   A. Shell support ['(N)PD'  means , of course, "(Not) public domain"].

      - Recommended shells:
 
        [UN*X BSD]:  - [bsh] = the Bourne shell [default: `/bin/sh'],
                     - [csh] = the C shell [default: `csh'],
        [MINIX]:     - [bsh] = the MINIX shell [default: `/bin/sh'],
        [ATARI.ST]:  - [msh] = the Mark Williams shell [`msh'] (NPD),
                     - [ash] = ASHELL.PRG [author: Jerry Nowlin] (PD)
                     - [bsh] = the Beckemeyer Micro C-shell [> 2.62](NPD)
   !                 - [gsh] = `gulam' [author: Prabhaker Mateti] (PD),
                     - [ssh] = `Craft 2.02' [author: Gert Poletiek] (NPD),
                     - [csh] = the Beckemeyer C-shell [`csh'] (NPD).
   !    [MACintosh]: - [???] = [none available]

   A1. Interactive use:

   1:  - BOOTing `lambda' from a shell: lambda <options>.
        NB: The LAMBDA-<options> are, in general, system-dependent.
   !        Some systems may support the <options> on stand-alone BOOTing.
   !        Check details with the current [Technical Notes], if present.

   2:  - A shell [is present in the current environment, but] inactive:

          mode [sh-]: leaves active at least the system [shell] commands: 
                      [ls][mem][du][pwd][cd][mkdir][rmdir][date][!]

   3:  - A shell is active and [the <internal/external shell-type> is] 
         recognized by `lambda':
 
          mode [sh+]: unrecognized external syntax is passed as such to 
                      the underlying shell, if this one is present in the
                      current environment, otherwise echo: 'No shell'.
 
   4:  - If the shell [-type] is not recognized: no echo (or side-effects!).

   !  - Change shell with [system-specific]: sys <shell-type>.
   !    [WARNING]: using two different `system()'-calls with the same
   !               shell can have unexpected side-effects.

   A2. Non-interactive [`batch'] processing: uses the underlying shell's 
       conventions for io-redirection (usually, UN*X-like).
  
       Examples:
 
         lambda < command-file                : reads commands from 
                                                <command-file> and
                                                writes to screen
         lambda < command-file > output-file  : ditto for reading, 
                                                writes to <output-file>
         lambda < command-file | some-other   : ditto for reading,
                                                sends output to 
                                                <some-other> reader.

       NB: On most systems, the <output-file> can be also a printer 
           and/or some other periferial [device].

   !   [WARNINGS]: 
   !     - LAMBDA is an INTERPRETER: a <command-file> must end with `exit'.
   !     - In non-interactive processing, it is recommended to disable 
   !       first the interactive mode of `lambda' [see command `talk-'].
 
   B. Stand-alone:

      - BOOTing `lambda': this is a system-specific operation 
        (e. g., on [MACintosh]: [CLICK-ON] `lambda'-icon).

      - NB: Shell-specific commands are ignored (echo: `No shell' on [sh+]).

   !  - NB: However, even on stand-alone BOOTing, the `lambda'-mode [sh+], 
   !        with the default shell <external-type> actually present in the  
   !        current environment has effect similar to sub-case A1:3 above.

   2.1. OPERATING `MODES'.

   A. Help:

      help                     Display a synoptic HELP-PAGE.

      local                    Display an overview of the LOCAL COMMANDS
                               currently available [system-dependent].

      ?                        Show current operating mode

   B. Set main operating options:

      lc                       LAMBDA-CALCULUS [BETA-] REDUCTIONS
                               [default on start-up]

      cl                       COMBINATOR REDUCTIONS/EXPANSIONS
                               [the expansions are done via `conv']

      conv                     CURRY ABSTRACTION ALGORITHMS
                               [= switch to code-generator]
                               [also a sub-option of the `cl'-mode]

   C. Set code-generation options [in `conv'-mode]:

      [conv] bc[+][-]          [de]activate the BC-code generation
                               [default: generate SK(I)-code only]

      [conv] ext[+][-]         [de]activate extensionality
                               [default: ext-][= generate "fat" code]

   D. Execute (= `eval'):
      [NB: The <term> list must be LISP-like! 
           If head-evaluation is required, use LIST-syntax!].    

      {do} (<term> ... <term>) reduce/expand <term>s
 
      See Examples under G. below.

   E. Trace to display-stream [NB: default to screen]:

      trace[+][-]              [de]activate the tracing [of executions]                                        
                               [default: trace+]

      [trace+] pp[+][-]        [de]activate the pretty-printer for traces
                               [default: pp-]

   F. Editing an ASCII-file with the built-in EDITor:
      NB: The editor currently built-in is a stripped-down version 
          of Ken Thompson's `ed', the "standard" UN*X line-editor.
          [ALTERNATIVE: uses `microEmacs' instead.]

      edit { <file> }          edit [ASCII] <file> with built-in EDITor
 
      NB: Without the <file> argument, the editor supplies a default 
          template (e. g., on a Macintosh, a temporary file `EditStuff').
          In such cases, DO `W[w](rite) <file>' to save the <file>.

   !  [WARNING]: On most systems, the built-in editor (`edit') requires
   !             a directory `tmp' in the operating environment. 
   !  NB: This convention does NOT apply to MACintosh [MFS] version(s)! 

      FEATURES:

          - Basic regular expression recognition ["standard"].

          - "Standard" commands: a(ppend),  c(hange),      d(elete), 
                                 E[e]dit,   f(ile),        g(lobal),
                                 i(nsert),  j(oin),        k(ey = mark),
                                 m(ove),    l(ist octal),  p(rint ASCII),
                                 Q[q](uit), r(ead),        s(ubstitute),
                                 u(ndo),    v(= global),   W[w](rite),
                                 (<line>)=  (= print <line> number).

          - Additional commands [NON-"standard"]:
            NB: The MACintosh-mode [MFS] supports [V <file>][H] only!

            !                    = escape to the current shell, if any
            V <file>             = VIEW <file> interactively = VISIT <file> 
            D                    = DISK usage of current working directory
            M                    = MEMORY currently available
            T                    = system date and TIME,
            L                    = LIST files on current working directory
            H                    = edit-HELP summary

          - VIEW/VISIT [sub-] mode: 
            NB: Following a `V <visited-file>' command, as for `cat', below.
            NB: These features are also NOT "standard"!
                                    
            b[B]                 = BACK = go to top of <visited-file>
            e[E] <file>          = EDIT <file> with built-in editor
            q[Q]                 = QUIT the current viewing [no changes]
            <other>              = go to the <visited-file>'s next page

      NB:  For a detailed documentation of the "standard" features of `ed', 
            - see KERNIGHAN & PIKE [84] 'Appendix I: Editor Summary',
            - see also `The UN*X Programmer's Manual' ED(1),
            - or do [on most UN*X-like systems]: `man ed'.

   G. PRE-PROCESSING the term-syntax [of the user-input]:

   ------------------------------------------------------------------------   
   |  If the term-syntax of the input is defective, the interpreter will  |
   |  report some diagnostics and attempt to recover parts of it in a     |
   |  usable form. The syntax error recovery feature CANNOT be switched   |
   |  off (!) but the verbosity of the diagnosis can. See [talk-] below.  |
   ------------------------------------------------------------------------

      talk+                    activate diagnostics on syntax error,
                               proceed interactively:
                                 IF <term-syntax-error>
                                   - guess user's intentions, 
                                   - propose a syntactically correct 
                                               recovery input,
                                   - ask user if he wants to evaluate
                                               recovered term(s),
                                   - on `y[Y]': evaluate,
                                   - on `n[N]': abort

      talk-                    deactivate diagnostics on syntax error,
                               non-interactive processing:
                                 IF <term-syntax-error>
                                   - guess user's intentions, 
                                   - propose a syntactically correct 
                                     recovery input,
                                   - evaluate recovered term(s).

   !  [WARNING]: Set ALWAYS [talk-] as a first command in <shell-script>s 
   !             processed non-interactively (e. g., while executing 
   !             processes like: `lambda < shell-script')!
      NB: This is NOT necessary in [read]-mode! E. g., on [talk+], a 
          command like `read <command-file-with-syntax-errors>' will 
          still cause the interpreter to ask your permission before 
          attempting to evaluate!

      NB: Intersticed SPACEs in non-critical positions are always ignored.

      Examples of input recovery (value depends on current execution mode:
      [lc] [cl] [conv] {[ext[+][-], bc[+][-]}) lib[+][-]).

      NB: analogous scripts work for [def][defnf][defrec] <name> = <term>.

           INPUT:            ACTION:
           ------            -------
           (BBB)           = evaluate (BBB)
           do (BBB)        = same as before
           (L(xx)x)        > evaluates to itself, (why?)
           NIL             > yields <don't-know-about-this> ?
           do (   )        > evaluates to () [= NIL]        ()
           ( (BIC) (CI) )  = evaluate (#(BIC)(CI)           (!)
           do ( BIS (CI) ) = evaluate (BIS(CI))             (!!)
           do (WWW)        > runs forever, without          (!!!)
                           > consumming space and/or memory (!!!)
           ( (WWW)(<this>) = ditto for (#(WWW)(<this>)),    (!!!!)
                           > we shall never reach <this>    (!!!!)
           ( B(BB(         = recovered as (B(BB#))          (!!!!!)
           do (BI))))      = recovered as (BI)              (!!!!!!)
                           > post-poned junk ignored        (!!!!!!)
           (BC)SSGARBAGE   = recovered as (BC)              (!!!!!!!)
           (S IS I)is(bad) = recovered as (SISI)            (!!!!!!!!)
                           > without post-poned rumors      (!!!!!!!!)
           ( S B           = recovered as (SB)              (!!!!!!!!!)
                           > evaluates to value of SUCC     (!!!!!!!!!)
                                 (( A N D ) ( S O ) ( O N... !!!!!!!!!)

   -----------------------------------------------------------------------
   | [MORALS] You may wisely use SPACEs in order to make terms readable! |
   |          Lazy people may always forget about closing parentheses!   | 
   |          Distracted people may always forget about LAMBDA-syntax!   |
   -----------------------------------------------------------------------

   2.2. IO MANAGEMENT. 

   A. Output back-up [history shell facility] and re-direction:
       NB: Certainly, the standard output is NOT de-activated on back-up.
       NB: The HELP- and the LOCAL-HELP pages are NEVER back-ed up!
    !  NB: The command `cat <file-to-visit>' with a <history-file> 
    !      switched on will also insert a copy of the <file-to-visit> 
    !      in the current <history-file>! However, `edit <file-to-edit>' 
    !      (the EDITor operations) are NOT backed up! Also, for obvious 
    !      reasons [whenever applicable], system- and shell-specific 
    !      actions from within `lambda' are NOT saved to a would-be
    !      <history-file>: this task is likely to be passed on to the 
    !      supporting shell, if any...

      open <history-file>      open a new <history-file>, 
                               back-up the current session to it 

      print+ <history-file>    activate back-up to the <history-file>

      print-                   deactivate back-up to current <history-file>.

   !  [WARNING]: If you forget the history shell tracing switched on, you 
   !             may sooner or later end up with no room left on the disk
   !             of the current working directory! 

   B. Standard IO operations [built-in commands]:
       NB: These commands do NOT need a shell.
       NB: On most systems, the <file> must be ASCII only.

      read <command-file>      read <command-file>, execute the contents 
 
      NB: If some shell is present, the <command-file> can be also used 
          as a shell script, within [sh+]-mode.

      cat <file>               view <file>, visit <file>,                                    
                               - b[B]    = BACK = go to top of <file>
                               - e[E]    = EDIT the <file> 
                               - q[Q]    = QUIT viewing the <file>
                               - <other> = go to the next page of <file>

      rm <file>                delete [= unlink] <file>,
 
   !  [WARNING]: Caution [it works nearly always]: no recovery after `rm'!
   !             E. g., try [on your risk] `rm Finder' on a MAC!

      sound[+][-]              [de]activate bell-warnings

   2.3. TERM LIBRARIES: 
 
   A. Default library of built-in terms:

      lib[+][-]                [de]activate library of built-in terms

      default-`lib' contents [standard documentation, see BUILT-IN ATOMS]:
  
        Resident term-library:  S, K, I, B, C, W (BARENDREGT [84])
                                [NB: `lib-' does NOT delete them!]

        Non resident built-in [lambda-] terms (in [lib+]-mode):

        J    : Rosser's J combinator (CHURCH [41])
        PI   : Church's PAIRing combinator (CHURCH [41])
        MU   : [Carew] Meredith's [last] generator (REZUS [82])
        PHI  : Curry's "formal substitution" PHI (BARENDREGT [84])
        PSI  : Curry's PSI combinator (BARENDREGT 84])
        SUCC : Church's SUCCESSOR [= SB] (CHURCH [41])
        SUM  : SUM on Church numerals (CHURCH [41])
        PROD : PRODUCT on Church numerals [= B] (CHURCH [41])
        EXP  : EXPONENTIATION on Church numerals [= CI] (CHURCH [41])
        0    : Church's numeral 0 [= KI = CK] (CHURCH [41])

   B. Current user definitions [internal term-library maintenace]:

       NB  [C, BCPL versions]: <name> is a single [upper-case] character.

       NB: Defining modulo normal forms, by `defnf', may fail [that is: 
           `lambda' would run forever] if the <term> is not normalizable 
           in standard reduction order (try `def' instead, on doubt). 
           
   !       Still, see the LOCAL COMMANDS on your specific system for 
   !       details on ABORTing non-terminating `lambda'-processes. 

       NB: Here, "current definition" means "current USER definition".

   B1. Defining modes:

      def <name> = <term>      define <name> as <term>
                            
      defnf <name> = <term>    define <name> as the normal form of <term>

      <name>  <  <term>        internal alias for `defnf <name> = <term>'        

      defrec <name> = <term>   recursive `def <name> = <term>'      
                               [E. g.: `defrec H = (SH(BH))', etc.]

   B2. User library maintenance [internal]:

      list                     list the current term-definitions

      show   <name>            show the current definition of <name> 

      copy   <name1> <name2>   define <name2> as definiendum of <name1>,
                               keep the current definition of <name1>  

      rename <name1> <name2>   re-define <name2> as <name1> and
                               forget the current definition of <name1>

      delete <name>            forget the current definition of <name>

      new                      forget all current definitions

   C. User library maintenace [external]:
   !   NB: The commands `put' and `get' may refuse to cope with user 
   !       <file>s that are not generated by the same version of `lambda'.
 
   !   NB: Internally, the [MAIN] interpreter tags a user library with 
   !       an initial reserved character (usually: @). User libraries  
   !       are stored in machine-readable format: do not edit them!.

       NB: Since the external term-libraries could be easily altered, 
           by inadvertent manipulations, it is advisable to generate 
           the basic [and/or frequently used] term-libraries in non-
           interactive mode or via a `read'-command, keeping always 
           backups for the generating [shell-] scripts. This precaution
           should also make term-libraries portable accross various 
           versions/"upgrades" of `lambda' and would spare a lot of 
           typing. As expected, such scripts can be also made/recovered 
           by editing the appropriate segment of a <history-file> that 
           has been saved previously.

      put <file>               save current user term-library to <file>

      get <file>               read user term-library from <file>.
      
   2.4. SYSTEM SUPPORTED COMMANDS: 
       NB: System-specific; check with the appropriate [Technical Notes].
       NB: On some systems, most of these commands may need a shell.
      
      !                        escape to the current shell
      sh[+][-]                 [de]activate the current shell
      sys                      change the current shell
      pwd                      show name of current working directory
      ls                       verbose list [ls -l] of cwd
      du                       show disk usage for cwd-unit [= UN*X `du .']
      cd <path>                change current directory to <path>
      mkdir <path>             make directory <path>
      rmdir <path>             remove directory <path>
      mem                      show memory available [= UN*X `quota'] 
      date                     show system date and time
      ed [ex][vi] {<file>}     call a system editor [`ed'; BSD: `ex', `vi']
      exit                     quit the [MAIN] interpreter.

      <any-other-string>       in [sh+]-mode: as interpreted by the 
                               current shell, if any

      NB: The `lambda'-commands have precedence over any would-be 
          identically labelled shell commands. In case of conflict, 
          one can still use the !-escape, or do an aliasing in the 
          current shell. Examples (1): 'ls' would always be verbose 
          on any UN*X-like system; (2): on ATARI.ST, with `gulam' as
          a current shell, do first 'alias  _help help' in order 
          to get help from `gulam' by asking `_help'. 
                               
   3. BUGS.
 
   3.1. [Internal bugs]: Most obvious bugs occurring in previous versions 
        of the [MAIN] interpreter have been removed. See also 4.0.

        NB: fixed from 1.28 on

        3.1.0: `read <command-file>' with non-existent <command-file>
               restores the default input stream with <file-not-found> 
               error: it doesn't crash the system [MAC][ATARI] any more.

        3.1.1: [MAC][ATARI][...]: single-key commands during evaluation
               [see: <system-specific> Technical Notes] allow to abort 
               stationary non-terminating LAMBDA-processes [e. g., 
               (WWW), etc.]

   3.2. [External bugs: malfunctions of the MAIN interpreter, arising
        from the co-operation with external/buggy/"hacking" programs]: 
 
        In general, the [MAIN] interpreter [i. e., the system-independent 
        segment of `lambda'] does not co-operate optimally with external
        programs that are "hacking into" the current system environment.

        Typically, external programs promoting a defective memory-
        management or interferring too aggressively with the current
        default setting of the periferials [console, keyboard, etc.] 
        would also crash those `lambda'-triggered processes that make 
        essential use of such system ingredients. Cases in point are 
        the [MAIN's] term-library management, the built-in EDITor 
        and the [VISIT/VIEW <file>]-functions. For instance, loading 
        alternate fonts [via overlays], without informing the system 
        about this, might cause bus/address [system] errors that won't 
        be currently catched by [`lambda'-] MAIN.

        On the other hand, the [MAIN] "lambda-reduction machine", as 
        well as the "combinatory code generator", have their private 
        security and error recovery routines and are unlikely to be 
        affected directly by "hacking programs". 
         
   3.3. [NOTE]. Further bug reports will be greatly appreciated. If you 
        take the trouble to notice a bug and are willing to mention it 
        to me, please, describe also in detail the environment used to 
        execute `lambda'-processes. Before doing this, notice that 
        `lambda' has not been originally intended for some particular 
        machine, although it is guaranteed to act as specified at 
        least with standard ASCII terminals and - whenever applicable 
        - in conjunction with a reasonable Bourne-like shell. Most 
        malfunctions that may count as "bugs" may be simply caused by 
        some strange habits of the keyboard on your local machine, 
        for instance or, by the use of a defective [external] shell-
        interpreter. 

   4. TO DO: 

   4.0. Comment: 
        ETA-reduction in [lc]-mode [current ver$] does NOT eliminate the
        ETA-redexes generated by a BETA-reduction. This is NOT a bug: 
        the interpreter proceeds in lazy-order. In order to remove all 
        ETA-redexes (!) one has to re-input evaluation results [currently 
        NOT supported (automatically)].

   4.1. YACC-parser for the command interpreter. Apparently NOT very
        useful for the current variant(s). Certainly needed for the next 
        four [4.2 - 4.5] items.

   4.2. Support for multi-character [word-length] term-definitions.
        [NB: This is available only in LISP versions of `lambda'.]

   4.3. Extension to typed lambda-calculus and typed combinators.

   4.4. Extension to the `Boolean' [typed] case.

   4.5. Addition of "non-standard" reduction strategies. 

   4.6. Windows & graphics shell management (e. g., a la GEM). 

   4.7. Transport to other systems.

   5. DATE OF LAST REVISION: 890304. Previous: [890226-0111-6][881111].

   6. STANDARD DISCLAIMER:
      "I make no warranty with respect to the contents of this document,
      or the software it describes, and disclaim any explicit and/or
      implied suggestions of usefulness for any particular purpose. 
      Use of the described software presupposes the fact that the user 
      is willing to assume all risks, and/or damages, if any, arising 
      as a result, even if it is caused by negligence, ignorance or 
      some other fault."       
