Взаимодействие с эффектами
Oct. 31st, 2012 02:08 pmРанее мы обозначили проблему декодирования результатов работы нашей системы (см. "Компиляция λ-выражений"). Это не новая проблема: "readback" известен своей сложностью в рамках темы оптимальной редукции, и едва ли не треть монографии на данной теме уделена "readback". Чтобы продолжить разработку нашего симулятора, нам потребуется разумное решение, которое бы подходило для нашей слепой стековой машины.
Напомним, что ранее мы ограничили множество λ-термов до λI-исчисления, чтобы упростить их компиляцию. Взамен мы получили право забыть об агентах ε, при этом не пожертвовав выразительными возможностями языка с точки зрения частичных рекурсивных функций. Теперь же мы дополнительно затребуем от вычисляемых выражений отсутствие свободных переменных. Это немного упростит "readback", избавив нас от рассмотрения особых случаев.
Итак, мы предполагаем некоторый λΙ-комбинатор. Головная нормальная форма λI-комбинатора всегда имеет вид λx1.…λxn.xi M1 … Mm, где m ≥ 0, n > 0, 0 < i < n. С точки зрения представлений в виде графов, подобных оптимальной редукции, - в том числе и в нашей системе слепой перезаписи - это, в частности, означает, что при условии наличия головной нормальной формы (в противном случае результат нас не интересует из-за бессмысленности выражения) становится возможным "readback" в виде следующей системы взаимодействия с побочными действиями:
Σ = {(ε, 0), (γ, 2), (ψ, 2), (c, 1), (@l, 2), (@r, 2)} ∪ {(xi, 0) | i ∈ N} ∪ {(λi, 1) | i ∈ N};
λi[λi(ε)] >< xj + "xj";
λi[a] >< γ[λi + 1(c(a)), xi] + "(λxi.";
xi >< ψ[xi, xi];
xi >< γ[a, @l(xi, a)];
λ[a] >< @l[λ(@r(b, a)), b] + "(";
λ[a] >< c[λ(a)] + ")";
λ[ε] >< @r[λ(c(a)), a] + " ".
Нетрудно проверить, что такое "readback"-взаимодействие не зависит от симуляции основной системы. Таким образом, выполнять "readback" можно даже по мере редукции, не дожидаясь ее завершения.
Напомним, что ранее мы ограничили множество λ-термов до λI-исчисления, чтобы упростить их компиляцию. Взамен мы получили право забыть об агентах ε, при этом не пожертвовав выразительными возможностями языка с точки зрения частичных рекурсивных функций. Теперь же мы дополнительно затребуем от вычисляемых выражений отсутствие свободных переменных. Это немного упростит "readback", избавив нас от рассмотрения особых случаев.
Итак, мы предполагаем некоторый λΙ-комбинатор. Головная нормальная форма λI-комбинатора всегда имеет вид λx1.…λxn.xi M1 … Mm, где m ≥ 0, n > 0, 0 < i < n. С точки зрения представлений в виде графов, подобных оптимальной редукции, - в том числе и в нашей системе слепой перезаписи - это, в частности, означает, что при условии наличия головной нормальной формы (в противном случае результат нас не интересует из-за бессмысленности выражения) становится возможным "readback" в виде следующей системы взаимодействия с побочными действиями:
Σ = {(ε, 0), (γ, 2), (ψ, 2), (c, 1), (@l, 2), (@r, 2)} ∪ {(xi, 0) | i ∈ N} ∪ {(λi, 1) | i ∈ N};
λi[λi(ε)] >< xj + "xj";
λi[a] >< γ[λi + 1(c(a)), xi] + "(λxi.";
xi >< ψ[xi, xi];
xi >< γ[a, @l(xi, a)];
λ[a] >< @l[λ(@r(b, a)), b] + "(";
λ[a] >< c[λ(a)] + ")";
λ[ε] >< @r[λ(c(a)), a] + " ".
Нетрудно проверить, что такое "readback"-взаимодействие не зависит от симуляции основной системы. Таким образом, выполнять "readback" можно даже по мере редукции, не дожидаясь ее завершения.
