compiler-construction - 无类型 Lambda 演算的函数式语言

Question

是否有无类型 lambda 演算的解释器（或编译器）？（根据这个线程这是可能的。）我认识到它作为一种编程语言几乎没有用，特别是如果许多语言（如数字和布尔运算符）是在（由用户或库）实现的语言本身。但是，我仍然认为这将是一个有趣的工具，对学习和探索微积分很有用。为此，解释器比编译器更可取，两者都可以。有人知道这样的程序吗？

Answer 1

You can use any untyped language that has lambda abstractions. For example Python or JavaScript. There are two main downsides:

1. These languages don't have lazy evaluation. This means that not all lambda terms will converge, even though they have a normal form. You have to take this into account and modify the task accordingly.
2. You won't see the result as a lambda-term in normal form. You have to know what to expect from the result and use the language to evaluate it to something that can be displayed.

Knowing this, let's make an example in Python: First we create helper functions to convert between numbers and Church numerals:

# Construct Church numeral from an integer
def int2church(n):
    def repeat(f, m, x):
        if (m == 0): return x
        else: return f(repeat(f, m-1, x))
    return lambda f: (lambda x: repeat(f, n, x))

def church2int(l):
    return l(lambda x: x + 1)(0)

now we can define standard operations on numerals:

zero = int2church(0)
one = int2church(1)

pred = lambda n: lambda f: lambda x: n(lambda g: lambda h: h(g(f)))(lambda u: x)(lambda u: u)

mul = lambda m: lambda n: (lambda f: m(n(f)))

expn = lambda n: lambda m: m(n)

tetra = lambda n: lambda m: m(expn(n))(one)

and compute for example 4³:

expn = lambda n: (lambda m: m(n))

a = int2church(4)
b = int2church(3)
print church2int(expn(a)(b))

or tetration:

a = int2church(5)
b = int2church(2)
print church2int(tetra(a)(b))

To be able to express even more interesting stuff, we can define the Y combinator:

y = lambda f: (lambda x: f(lambda v: x(x)(v))) (lambda x: f(lambda v: x(x)(v)))

and compute for example factorials:

true = lambda x: (lambda y: x)
false = lambda x: (lambda y: y)

iszero = lambda n: n(lambda x: false)(true)

fact = y(lambda r: lambda n: iszero(n)(one)(mul(n)(lambda x: r(pred(n))(x))))
print church2int(fact(int2church(6)))

Note that the Y combinator had to be adapted for strict evaluation using η-expansion, as well as the factorial function to avoid infinite recursion due to strict evaluation.

Answer 2

Benjamin Pierce 提供了无类型和简单类型λ 演算的实现，伴随着他的教科书类型和编程语言。它们是用 OCaml 编写的，并包含示例定义。然而，为简单的 λ-calculi 编写解释器或编译器应该不难。

Answer 3

使用一些技巧，这几乎可以在任何函数式语言中完成。至少我在 Haskell 和 OCaml 中看到过类似的东西。但是，有时您必须绕过类型系统的限制。通常，您通过将其实现为统一系统来获得“无类型”功能。所以每个 lambda 函数都会有类型

type lambda = lambda -> lambda

在默认设置中，例如 OCaml 不允许这样的递归类型，但可以通过定义来规避这种情况：

type lambda = L of lambda -> lambda

Answer 4

我是函数式编程课程的助教。出于教学目的，我们将这个在线lambda 演算归约器视为探索微积分的有趣且有用的工具。如果您想使用它，他们也有可用的 SML 源代码。

Answer 5

我写了一篇，今年早些时候。 在这里。

Answer 6

I created a web hosted interpreter for a lambda calculus based language I call pureƒn in an effort to learn the workings of the Lambda Calculus. It may be useful for people wanting to learn and experience some of the fundamental principles of computer science in an interactive manner with minimal notation complexity.

pureƒn is a programming environment based on the functionality of the Lambda Calculus, but with a simplified notation. pureƒn allows for the definition, application and reduction of functional abstractions. The notation and syntax are minimal yet sufficient to allow the underlying concepts to be easily understood.

The underlying compiler was written in Python and compiles the abstractions into functions that reduce to normal form (if possible) automatically when applied to each other. This means that if you define the S, K and I combinator functions, and then apply them as S K K, the function that gets returned will be the I function, not just a function that behaves like I, meaning that the following would hold true:

>>>S(K)(K) is I
True

Answer 7

Here is one written in Python. It appears to be very immature, but it is an interesting start of implementing one Python. It depends on the module ply.

Here is another one (sort of) for C++—very interesting.

If your main intention is to get some basic automation involved in learning lambda calculus (for example, trying to derive arithmetic operations for yourself) and particular Church numerals and booleans, a primitive but easy-to-implement solution is to limit yourself to a small subset of Python, in which you can define your own Church numerals and operators, and check them by functions which convert them into the regular Python types. A function to do this for Church numerals:

lambda churchnum: churchnum(lambda x: x+1)(0)

And one for Church booleans:

lambda churchbool: churchbool(True)(False)