Ответ 1
Суть комбинатора с фиксированной запятой C
заключается в том, что C f
сводится к f (C f)
. Неважно, что вы делаете для C
, пока это делается. Поэтому вместо
(\y f. f (y y f)) (\y f. f (y y f))
вы можете просто взять
(\y z f. f (y y y f)) (\y z f. f (y y y f)) (\y z f. f (y y y f))
В принципе вам нужно что-то вроде формы
C t1 t2 ... tN
где ti = C
для некоторых i
и
C = \x1 x2 .. xN f. f (xi u1 u2 ... xi ... u(N-1) f)
Другие термины tj
и uj
фактически не используются. Вы можете видеть, что Klop L
имеет эту форму (хотя он использует тот факт, что все ti
являются L
такими, что второй xi
также может быть любым другим xj
).