[Club2] 22.03: 15.00 Uhr, !!!ZUSE!!!

[Norbert Schirmer]

Diese Woche:

Mi. 22.03: 15.00 Uhr im Zuse (01.11.018)

Christian Urban:

Nominale Unifikation
=2D-------------------

Ich werde einen einfachen Algorithmus pr=E4sentieren,=20
der Terme modulo alpha-Equivalenz unifiziert. Mit=20
diesem Algorithmus kann man zum Beispiel recht=20
einfach folgendes Quiz l=F6sen:

  Assuming that a and b are distinct variables, is it possible=20
  to find lambda-terms M_1 to M_7 that make the following=20
  pairs alpha-equivalent?

      \lambda a.\lambda b. (M_1 b) and \lambda b.\lambda a. (a M_1)

      \lambda a.\lambda b. (M_2 b) and \lambda b.\lambda a. (a M_3)

      \lambda a.\lambda b. (b M_4) and \lambda b.\lambda a. (a M_5)

      \lambda a.\lambda b. (b M_6) and \lambda a.\lambda a. (a M_7)

  If there is one solution for a pair, can you describe all its=20
  solutions?


   Norbert