Reto N.2 7-9-2020

gistfile1.txt

Reduzca a forma normal las siguientes abstracciones:
1. (\x.xx)(\x.xx)
2. (\x.xxx)(\x.xxx)
3. (\x.\y.xy)(\y.y)e  # Para evitar confusion, use una abstraccion Alpha-equivalente para el combinador Identidad

4. (\m.\n.(
      (n (\a.\b.\c.
        (
          b((ab)c)
        )
      ))m
    )
  ) (\f.\n.n) (\f.\n.fx)

5. (\a.a)(\b.b)(\c.cc)(\d.d)

Reduzca a forma normal las siguientes abstracciones:

aplicacion de funciones

1. (\x.xx)(\x.xx) --> M := e | x | MM | \x.M
   (\x.xx)(\x.xx)

   (\a.aa)(\b.bb)
   (\b.bb)(\b.bb)

2. (\x.xxx)(\x.xxx)
   (\c.c c c)(\a.aaa)
   (\a.aaa) (\a.aaa) (\a.aaa)

   (\x.xxx)(\x.xxx)
   (\b.bbb)(\w.www) (\a.aaa)
   (\z.zzz)(\p.ppp)(\w.www)(\a.aaa)
   (\p.ppp)(\p.ppp)(\p.ppp)(\w.www)(\a.aaa)
   Halting problem

3. (\x.\z.xz)(\y.y)e # Para evitar confusion, use una abstraccion Alpha-equivalente para el combinador Identidad
   (\z.(\y.y)z)e
   (\y.y)e
   e

Funciones (de) punto fijo
Fixed point functions

(\a.aa)(\b.bb) --> quan
(\y.y)e

4. (\m.\n.(
   (n (\a.\b.\c.
   (
   b((ab)c)
   )
   ))m
   )
   ) (\f.\n.n) (\f.\n.fx)

M::(\f.\n.n)
N::(\f.\n.fn)
F::(\a.\b.\c.(b((ab)c)))

(\m.\n.( (n F )m)) M N
(\n.( (n F )M)) N
(NF)M
( (\f.\n.fn)(\a.\b.\c.(b((ab)c))) )M
( (\n.(\a.\b.\c.(b((ab)c)))n) )M
(\n.(\a.\b.\c.(b((ab)c)))n) M
(\a.\b.\c.(b((ab)c)))M
(\b.\c.(b((Mb)c)))
(\b.\c. (b( ( (\f.\n.n) b) c) ))
(\b.\c. (b( (\n.n)c ) ))
(\b.\c.bc) --> Beta normal

1+0=1
Peano numerals

"0" :: (\f.\x.x)
"1" :: (\f.\x.fx)
"2" :: (\f.\x.ffx)
(N+1)th :: SUCC N -> (\a.\b.\c.(b((ab)c)))

SUCC 2 ->> (\f.\x.fffx)
(\a.\b.\c.(b((ab)c))) 2
\b.\c.b(2b)c
\b.\c.b( (\f.\x.ffx) b)c
\b.\c.b (\x.bbx)c
\b.\c.b bbc
\b.\c.bbbc == (\f.\x.fffx)

5. (\a.a)(\b.b)(\c.cc)(\d.d)
   (\b.b)(\c.cc)(\d.d)
   (\c.cc)(\d.d)
   (\d.d)(\d.d)
   (\d.d)