项目作者: zhiayang

项目描述 :
lambda calculus interpreter
高级语言: C++
项目地址: git://github.com/zhiayang/lambda.git
创建时间: 2021-03-30T15:52:34Z
项目社区:https://github.com/zhiayang/lambda

开源协议:Apache License 2.0

下载


lambda calculus interpreter

what:

A small lambda calculus interpreter written in C++. It supports α-conversion and β-reduction,
as well as precise tracing output of replacements and renames.

how:

The standard lambda calculus syntax is supported, eg:

  1. z.(((λx.(λy.x)) z) ((λx.(λy.x)) z)))

Note that variable names can be multi-character, so they must be separated with spaces. Syntax sugar
for multi-argument functions is supported:

  1. λx y.x == λxy.x

Haskell-style lambda syntax is also supported, because nobody knows how to type λ:

  1. \x y -> x == \x -> \y -> x

Let-bindings are also supported:

  1. let S = \x y z -> x z (y z)
  2. let K = \x y -> x
  3. let I = \x -> x
  4. S K K == I

If the FLAG_VAR_REPLACEMENT flag (toggle with :v) is used, the interpreter will attempt to back-substitute the
end result of an evaluation by using alpha-equivalence; for example, when doing S K K, instead of showing λx.x,
it will show I if an alpha-equivalent definition of I is available.

load

You can load files from the command line simply by passing them as arguments to the interpreter, eg.

  1. $ build/lc lib/ski.lc

You can also use the :load directive, either in the REPL or in a file itself (so you can do recursive includes).
Note that include loops are not handled, and you’ll crash the interpreter.

example

Here is some example output:

  1. *. parenthesis omission enabled
  2. *. curried abbreviation enabled
  3. *. haskell-style printing enabled
  4. *. loaded 13 lines from 'lib/ski.lc'
  5. λ> S K K
  6. 0. (\x y z -> x z (y z)) (\x y -> x) (\x y -> x)
  7. 1. β-red: x <- (\x y -> x)
  8. 2. β-red: y <- (\x y -> x)
  9. 3. β-red: x <- z
  10. 4. β-red: y <- (\x y -> x) z
  11. *. done.
  12. (\z -> z)
  13. λ>

repl commands

command function
:q quit the repl
:t enable (basic) tracing (shows α and β steps)
:ft enable full tracing (detailed substitution)
:v enable back-substitution for the result
:p enable omitting unambiguous parentheses when printing
:c enable shorthand notation when printing curried functions
:h enable haskell-style notation when printing
:load load a file (eg. :load foo.lc) and add it to the context