Ромбовидное свойство отношений. Редукционный граф бета-редукции. Отсутствие у бета-редукции ромбовидного свойства. Отношение бета-редуцируемости. Назовём отношение R обладающим ромбовидным свойством, если из того, что aRb и aRc следует, что найдётся элемент d, такой, что bRd и cRd.
Так как бета-редукция является бинарным отношением, можно изобразить её граф или часть его. Если изображаются только термы, которые можно получить из некоторого терма A путём n шагов бета-редукции всевозможных его частей (n >= 0), то такой граф называется редукционным графом терма A.
Заметим, что отношение бета-редукции НЕ обладает ромбовидным свойством. Действительно, рассмотрим терм w (I d). Очевидно, редуцируя внутренний редекс, за 2 шага приходим к нормальной форме, в то время как редуцируя внешний, до нормальной формы добираемся за 3 шага. Таким образом, этот терм является контрпримером к утверждению о существовании ромбовидного свойства у бета-редукции.
Отношением бета-редуцируемости называется рефлексивное и транзитивное замыкание отношения бета-редукции. Теорема Чёрча-Россера утверждает о наличии ромбовидного свойства у отношения бета-редуцируемости.