η-редукция в сетях взаимодействия
Apr. 9th, 2013 10:15 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
codedothttp://mathoverflow.net/questions/126941/
Существуют несколько способов представить λ-термы в сетях взаимодействия; например, алгоритм Лэмпинга для оптимальной редукции или компиляция λ-исчисления в комбинаторы взаимодействия. Однако, все известные нам способы реализуют только β-редукцию, но не экстенсиональное λ-исчисление (где также есть η-редукция).
Можно ли представить λ-термы в сетях взаимодействия, реализовав βη-редукцию?
(Нормальная форма сети для терма должна соответствовать его βη-нормальной форме.)
Существуют несколько способов представить λ-термы в сетях взаимодействия; например, алгоритм Лэмпинга для оптимальной редукции или компиляция λ-исчисления в комбинаторы взаимодействия. Однако, все известные нам способы реализуют только β-редукцию, но не экстенсиональное λ-исчисление (где также есть η-редукция).
Можно ли представить λ-термы в сетях взаимодействия, реализовав βη-редукцию?
(Нормальная форма сети для терма должна соответствовать его βη-нормальной форме.)
