Dennis_Callanan_Semantics_Assignment

Form 1 - Input


(λ a . (λ b . (λ c . (λ d . (λ n m f x . n f (m f x)) ((λ n m f . n (m f)) ((λ n m . m ((λ n m f . n (m f)) n) ((λ n f x . n f (f x)) (λ f x . x))) d ((λ n f x . n f (f x)) ((λ n f x . n f (f x)) (λ f x . x)))) c) ((λ n m f . n (m f)) c ((λ n f x . n f (f x)) d))) ((λ n m f x . n f (m f x)) b b)) ((λ n f x . n f (f x)) b)) ((λ n m f x . n f (m f x)) a ((λ n f x . n f (f x)) ((λ n f x . n f (f x)) (λ f x . x))))) ((λ n f x . n f (f x)) ((λ n f x . n f (f x)) ((λ n f x . n f (f x)) (λ f x . x))))


Form 2 - indented

(λ a .
    (λ b .
        (λ c .
            (λ d .
                (λ n m f x . n f (m f x))
                (
                    (λ n m f . n (m f))
                    (
                        (λ n m . m ((λ n m f . n (m f)) n) ((λ n f x . n f (f x)) (0))) d
                        (
                            (λ n f x . n f (f x))
                            (
                            (λ n f x . n f (f x))
                            (0)
                            )
                        )
                    )
                    c
                )
                (
                (λ n m f . n (m f)) c
                (
                (λ n f x . n f (f x)) d
                )
                )
            )
            (
            (λ n m f x . n f (m f x))
                b
                b
             )
        )
        (
            (λ n f x . n f (f x)) b))
            (
                (λ n m f x . n f (m f x))
                a
                (
                    (λ n f x . n f (f x))
                    (
                        (λ n f x . n f (f x)) (0)
                    )
                )
            )
)
(
    (λ n f x . n f (f x))
    (
        (λ n f x . n f (f x))
        (
            (λ n f x . n f (f x))(0)
        )
    )
)


======================================

0  = 1 = λ f . (λ x . x)
1  = λ f x . f x
2  = λ f x . f (f x)
3  = λ f x . f (f (f x))
4  = λ f x . f (f (f (f x)))
5  = λ f x . f (f (f (f (f x))))

===================================

SUCC = λ n . (λ f x . f (n f x))
or
SUCC = λ n . (λ f x . n f (f x))

PLUS = λ n m . λ f x . m f (n f x)
or
PLUS = λ n m . λ f x . n f (m f x)

mult = (MULT)

=======================================


Form 2 - Perform substitutions:


(λ a .
    (λ b .
        (λ c .
            (λ d .
                (PLUS)
                (
                    (MULT)
                    (
                        (λ n m . m ((MULT) n) ((SUCC) (0))) d
                        (
                            (SUCC)
                            (
                            (SUCC)
                            (0)
                            )
                        )
                    )
                    c
                )
                (
                (MULT) c
                (
                (SUCC) d
                )
                )
            )
            (
            (PLUS)
                b
                b
             )
        )
        (
            (SUCC) b))
            (
                (PLUS)
                a
                (
                    (SUCC)
                    (
                        (SUCC) (0)
                    )
                )
            )
)
(
    (SUCC)
    (
        (SUCC)
        (
            (SUCC)(0)
        )
    )
)





Form 4 - Continue substituting:


(λ a .
    (λ b .
        (λ c .
            (λ d .
                (PLUS)
                (
                    (MULT)
                    (
                        (λ n m . m ((MULT) n) ((SUCC) (0))) d
                        (
                            (SUCC)
                            (
                            (SUCC)
                            (0)
                            )
                        )
                    )
                    c
                )
                (
                (MULT) c
                (
                (SUCC) d
                )
                )
            )
            (
            (PLUS)
                b
                b
             )
        )
        (
            (SUCC) b)
     )
            (
                (PLUS)
                a
                (
                    (SUCC)
                    (
                        (SUCC) (0)
                    )
                )
            )
)
(3)



Form 4: Initialize reduction:


(λ b .
    (λ c .
        (λ d .
            (PLUS)
            (
                (MULT)
                (
                    (λ n m . m ((MULT) n) ((SUCC) (0))) d
                    (
                        (SUCC)
                        (
                        (SUCC)
                        (0)
                        )
                    )
                )
                c
            )
            (
            (MULT) c
            (
            (SUCC) d
            )
            )
        )
        (
        (PLUS)
            b
            b
         )
    )
    (
        (SUCC) b)
 )
        (
            (PLUS)
            (3)
            (
                (SUCC)
                (
                    (SUCC) (0)
                )
            )
        )




From 5 - Continue reducing:


 (λ c .
    (λ d .
        (PLUS)
        (
            (MULT)
            (
                (λ n m . m ((MULT) n) ((SUCC) (0))) d
                (
                    (SUCC)
                    (
                    (SUCC)
                    (0)
                    )
                )
            )
            c
        )
        (
        (MULT) c
        (
        (SUCC) d
        )
        )
    )
    (
    (PLUS)
        (5)
        (5)
     )
    )
(6)


Form 6 - Further reductions:


(λ d .
    (PLUS)
    (
        (MULT)
        (
            (λ n m . m ((MULT) n) ((SUCC) (0))) d
            (
                (SUCC)
                (
                (SUCC)
                (0)
                )
            )
        )
        (6)
    )
    (
    (MULT) (6)
    (
    (SUCC) d
    )
    )
)
(10)



Form 7 - Simplification:


(PLUS)
(
    (MULT)
    (
        (λ n m . m ((MULT) n) ((SUCC) (0))) (10)
        (
            (SUCC)
            (
            (SUCC)
            (0)
            )
        )
    )
    (6)
)
(
(MULT) (6)
(
(SUCC) (10)
)
)



Form 8 - Further simplification:

(PLUS)
(
    (MULT)
    (
        (2) (MULT) (10) (1)
    )
    (6)
)
(66)



Form 10 - Concluding

(PLUS)
(20)
(6)
(66)

Form 11 - Complete solution

(26)
(66)

We can write this in the following form:

λ f x . f (f (f (f .... (f x)))) λ f x . f (f (f (f .... (f x))))
            26 fs                               66 fs