$blog→errstr

do not commit

On Our Way to Reduction: Implement Substitution

| Comments

Introduction

Now that I have the mathematical definition of substitution, I can implement it. For ease of implementation, I will not consider call by name substitution which requires alpha-conversion. I will implement call by value, which is what most familiar programming languages use, such as Python, Ruby, PHP, C, Perl, and Java to name a few.

Substitution: Recursive Definition with Alpha Conversion

# Replace all free occurrences of x in x with s
[x ↦ s]x        = s
# Replace all free occurrences of x in y with s
[x ↦ s]y        = y     if x ≠ y
# Replace all free occurrences of x in λy.t1 with s
[x ↦ s](λy.t1)  = λy.[x ↦ s]t1  if y ≠ x and y ∉ FV(s)
# Replace all free occurrences of x in t1 t2 with s
[x ↦ s](t1 t2)  = ([x ↦ s]t1)([x ↦ s]t2)

Strategy

I basically have four things to consider when substituting in call by value: * If the term is in the form [x ↦ s]x, return the value s * If the term is in the form [x ↦ s]y, return the term y, since x ≠ y * If the term is in the form [x ↦ s](λy.t1), return the substituted abstraction λy.[x ↦ s]t1 * If the term is in the form [x ↦ s](t1 t2), return the application where each term is substituted ([x ↦ s]t1)([x ↦ s]t2)

There are three parts to every substitution: term, variable, and value. So I will need them as parameters to my function; I’ll call them term var value. In mathematical format, you can think of it like this: [var ↦ value]term.

Implementation in Racket

Using a functional language, like Racket, allows us a more powerful, terse, and elegant solution to the substitution function. I employ the use of Racket’s match which gives extremely powerful pattern matching.

(define (subst term var value)
  (match term
    ; [x -> s]y -> y = x ? s : y
    [(? symbol?) (if (eq? term var) value term)]
    ; [x -> s]λx.b -> λx.b
    ; [x -> s]λy.b -> λy.[x -> s]b
    [`(λ (,v) ,body) (if (eq? v var) term `(λ (,v) ,(subst body var value)))]
    ; [x -> s](t1 t2)
    [`(,f ,a) `(,(subst f var value) ,(subst a var value))]))

Tests

> (subst `(λ (x) 'y) 'y '1)
'(λ (x) (1))

> (subst `(λ (x) 'y) 'y `(λ (x) 'z))
'(λ (x) ((λ (x) 'z)))

> (subst `((λ (x) y) (λ (y) z)) 'z '2)
'((λ (y) 2))

> (subst `((λ (x) y) (λ (y) z)) 'y '2)
'((λ (y) z))

On Our Way to Reduction: Substitution

| Comments

Introduction

The ability to properly substitute is vital to reduction. In this post, I will show proper and improper definitions of substitution.

Semantics Primer

From my earlier post on currying you would have seen a substitution syntax like this, (λx.t1)t2 ↦ [x ↦ t2]t1 where [x ↦ t2]t1 means the term obtained by replacing all free occurrences of x in t1 by t2. See my last post for the definition of free variables.

Some Wrong Ways to Do It

The definition of the λ-calculus is simple. We have a term broken into three additional parts: variable, abstraction, and application. To define substitution, we must define it for the each part of a term. For variables, it must be defined when there is a free variable and when there is not. ###Naive Recursive Definition

# Replace all free occurrences of x in x with s
[x ↦ s]x        = s
# Replace all free occurrences of x in y with s
[x ↦ s]y        = y     if x ≠ y
# Replace all free occurrences of x in λy.t1 with s
[x ↦ s](λy.t1)  = λy.[x ↦ s]t1
# Replace all free occurrences of x in t1 t2 with s
[x ↦ s](t1 t2)  = ([x ↦ s]t1)([x ↦ s]t2)

The problem with the definition from above is that we are relying on the name of the variable or term to define substitution. This works fine if we are careful with our choice of bound variable names, however take the example [x ↦ y](λx.x). If we replace all free x terms within the abstraction λx.x with y we would end up with the following: λx.y, clearly this is no longer the identity function.

What should be taken away from this? The names of bound variables do not matter

Almost Fixed Definition

Let’s ensure that names of bound variables don’t matter.

# Replace all free occurrences of x in x with s
[x ↦ s]x        = s
# Replace all free occurrences of x in y with s
[x ↦ s]y        = y     if x ≠ y
# Replace all free occurrences of x in λy.t1 with s
[x ↦ s](λy.t1)  = λy.t1         if y = x
[x ↦ s](λy.t1)  = λy.[x ↦ s]t1  if y ≠ x
# Replace all free occurrences of x in t1 t2 with s
[x ↦ s](t1 t2)  = ([x ↦ s]t1)([x ↦ s]t2)

So, in this case, [x ↦ y](λx.x) = λy.y which is indeed the identity function. However, this is still wrong. Take this example: [x ↦ z](λz.x). Using the definition above, we would be substituting z for all free variables in (λz.x) which would leave us with λz.z, the identity function. But λz.x is not the identity function. So names are still an issue.

Variable Capture and Capture Avoidance

When a free variable in a term s is bound when s is substituted into a term t naively is called variable capture. We want to avoid this. We do this by using a substitution operation that avoids mixing bound variable names of t and free variable names of s. This is called capture-avoiding substitution and is often what is implicitly meant by the term substitution. It is easily achieved by one more condition on the abstraction case:

# Replace all free occurrences of x in x with s
[x ↦ s]x        = s
# Replace all free occurrences of x in y with s
[x ↦ s]y        = y     if x ≠ y
# Replace all free occurrences of x in λy.t1 with s
[x ↦ s](λy.t1)  = λy.t1         if y = x
[x ↦ s](λy.t1)  = λy.[x ↦ s]t1  if y ≠ x and y ∉ FV(s)
# Replace all free occurrences of x in t1 t2 with s
[x ↦ s](t1 t2)  = ([x ↦ s]t1)([x ↦ s]t2)

This however, is not a complete definition, since it has now changed substitution into a partial operation. For example: [x ↦ y z](λy.xy) should equal λy.yzy, but because it does not appear free in (y z) it never hits one of our definitions.

A Convention: Alpha-Conversion

In order to fix the issue of bound and free variable names, we must decide to work with terms “up to renaming of bound variables” or what Church called alpha-conversion. This is the operation of consistently renaming a bound variable in a term. In other words, “Terms that differ only in the names of bound variables are interchangeable in all contexts”.

This actually simplifies our definition, since we can change names as soon as we get to a place where we are trying to apply the substitution to arguments where it is undefined. This means we can completely drop the first clause of the abstraction section.

Final Definition

# Replace all free occurrences of x in x with s
[x ↦ s]x        = s
# Replace all free occurrences of x in y with s
[x ↦ s]y        = y     if x ≠ y
# Replace all free occurrences of x in λy.t1 with s
[x ↦ s](λy.t1)  = λy.[x ↦ s]t1  if y ≠ x and y ∉ FV(s)
# Replace all free occurrences of x in t1 t2 with s
[x ↦ s](t1 t2)  = ([x ↦ s]t1)([x ↦ s]t2)

On Our Way to Reduction: Free Variables

| Comments

Introduction

The ability to reduce is one of the key components to the λ-calculus. However, you find it directly implemented in compiler optimizations for both functional and imperative languages and as inspiration in Google’s MapReduce.

However, there are some subtleties that must be addressed to go from our λ and λNB calculi to being able to implement reduction. In this post, I mathematically prove that reduction on the λ-calculus terms can be done.

Define The λ-Calculus

As I described in my initial post about the λ-calculus, it is a very simple definition:

t ::=           terms:
    x         variable
    λx.t   abstraction
    t t    application

Definition of a Set of Free Variables and Size

Free variables are defined as:

FV(x)       = {x}
FV(λx.t1)   = FV(t1) \ {x}
FV(t1 t2)   = FV(t1) ∪ FV(t2)

Size is defined as:

size(true)                  = 1
size(false)                 = 1
size(0)                     = 1
size(succ t1)               = size(t1) + 1
size(pred t1)               = size(t1) + 1
size(iszero t1)             = size(t1) + 1
size(if t1 then t2 else t3) = size(t1) + size(t2) + size(t3) + 1

Proof that |FV(t)| ≤ size(t)

Unlike many statements in math, intuition and reality are in sync on this statement. Of course the statement { ∀ t, FV(t) ≤ size(t) } is true. However, it is important to formally prove this, since this is key to reduction.

By induction, by proving the following three cases, we can prove the statement to be true for all t:

Case 1:

t = x
|FV(t)| = |{x}| = 1 = size(t)

Case 2:

t = λx.t1
Inductively:
|FV(t1)| ≤ size(t1)
So:
|FV(t)| = |FV(t1) \ {x}| ≤ |FV(t1)| ≤ size(t1) < size(t)

Case 3:

t = t1 t2
Inductively:
|FV(t1)| ≤ size(t1) and |FV(t2)| ≤ size(t2)
So:
|FV(t)| = |FV(t1) ∪ FV(t2)| ≤ |FV(t1)| + |FV(t2)| ≤ size(t1) + size(t2) < size(t)

Z-Combinator and Factorial in Perl

| Comments

Introduction

Since I just did an implementation of the Z-combinator and Factorial in Python, I figured it would be fun to implement in Perl, too. It’s a lot uglier in Perl than Python, but Python is cheating with having a built-in lambda operator.

Implementation

Z = λf. (λx. f (λy. x x y))(λx. f (λy. x x y))
g = λfct. λn. if realeq n c0 then c1 else (times n (fct (prd n))) ;
factorial = Z g
#!/usr/bin/env perl

use warnings;
use strict;

my $Z = sub {
    my ($f) = @_;
    return (sub {
        my ($x) = @_;
        return $f->(sub {
            my ($y) = @_;
            return $x->($x)->($y);
        });
    })->(sub {
        my ($x) = @_;
        return $f->(sub {
            my ($y) = @_;
            return $x->($x)->($y);
        });
    })
};

my $g = sub {
    my ($fct) = @_;
    return sub {
        my ($n) = @_;
        return !$n ? 1 : $n * $fct->($n-1);
    };
};

my $factorial = $Z->($g);

print map { $factorial->($_)."\n" } @ARGV;

So what is the output?

./thelambda.pl 3 5 100
6
120
9.33262154439441e+157