![]() Revert renaming of bound variables, i.e. ![]() ( define ( evec x ) ( contract ( rename ( expand x ) ' evec ))) Convert terms to evec notation see "Compiling Lambda Calculus" ( ) for an explanation ((lam x (lam y x)) (lam x x)) -> ((lam 0 (lam 1 0)) (lam 0 0)) ![]() ( define ( pnf x ) ( contract ( rename ( expand x ) ' pnf ))) Convert normal forms to Church principal NFs (PNFs), i.e.: (lam x (lam y z)) -> (lam a (lam b c)) ( string-append "_" ( number->string sub )) Renaming Bound Variables Rename the bound variables of a lambda term, e.g. (define (interrupted?) #f) Write output to the terminal and, optionally, a log file Source Code Renaming Bound Variables Resolving Definitions Expanding and Contracting Abbreviations Pretty-Printing Reduction Encoding and Decoding Church Numerals Common Definitions Read Eval Print Loop - Lambda Calculator By Nils M Holm, 2016, 2017 Provided under the Creative Common Zero (CC0) license ( ) Example: (nr '((lam (x y z) y) M N)) -> (lam z N) (repl) will start a REPL ? will print help - If your Scheme has "char-ready?", ENTER can be used to interrupt reductions ( define ( interrupted? ) ( char-ready? )) reduction tracing (prints all one-step reductions).transformation to principal normal form.transformation to/from abbreviated form. ![]() applicative-order reduction (restricted λK-calculus).normal-order (left-to-right, outside-in) reduction.Source code below or just download the program: lc.scm A function collection and REPL for the λKβ- and ![]()
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |