Geek Answers Handbook

Functional language for untyped calculus lambda

Is there an interpreter (or compiler) for untyped lambda calculus? (According to this thread, this is possible.) I understand that it will be of little use as a programming language, especially if most of the language (for example, numbers and logical operators) were implemented (either by the user or by the library) in the language itself. However, I still believe that it would be a useful tool for studying and studying calculus. For this, the interpreter will be preferable to the compiler, or it will work. Does anyone know about such a program?

+5
source share
7 answers

Benjamin Pierce provides untyped implementations and simply typed λ-calculus, which accompanies his tutorial Types and Programming Languages . They are written in OCaml and include example definitions. However, it is not difficult to write an interpreter or compiler for simple λ-calculi.

+6
source

You can use any untyped language with lambda abstractions. For example, Python or JavaScript. There are two main disadvantages:

  • These languages ​​do not have a lazy rating. This means that not all lambda members converge, even if they have a normal shape. You must take this into account and change the task accordingly.
  • - . , , , , .

, Python: :

# 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)

:

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)

, , 4 3:

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

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

tetration:

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

, Y combinator:

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

, , :

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)))

, Y combinator η-, , - .

+7

, . , - Haskell OCaml. . "" , . -

type lambda = lambda -> lambda

, , OCaml , , , :

type lambda = L of lambda -> lambda
+3

- . - -

+3

, . .

+2

- , -, pureƒn, . , .

pureƒn - , Lambda Calculus, . pureƒn , . , , .

Python , ( ) . , S, K I, SKK, , , I, , I, , :

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

Python. , Python. ply.

- () ++ - .

, , - (, ) , , - Python, , Python. :

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

:

lambda churchbool: churchbool(True)(False)
0

More articles:


All Articles