Как можно превратить бесконечные

Я думал об этих вопросах:

Существует ли типизированное лямбда-исчисление, которое является последовательным и полным по Тьюрингу?

/cs/65003/if-%CE%BB-xxx-has-a-type-then-is-the-type-system-inconsistent

и уже нет трудно ответить на связанные вопросы в нетипизированной обстановке! В частности, мне любопытно узнать, можем ли мы восстановить полноту по Тьюрингу из не прекращения следующим образом:

Вопрос: Учитывая (чистый) $\lambda$ -term $t$ с не слабой головной нормальной формой, не существует всегда существует фиксированная точка комбинатора $Y_t$ такие , что

$$Y_t\ (\lambda x.x) = t$$

Все равенства взяты по модулю $\beta\eta$ .

Я на самом деле подозреваю, что эта версия вопроса неверна , поэтому можно смягчить вопрос для циклических комбинаторов , где циклический комбинатор $Y$ определен так, что для каждого $f$

$$Y\ f=f\ (Y'\ f)$$ где $Y'$ снова требуется быть циклическим комбинатором. Конечно, этого достаточно для определения рекурсивных функций как обычно.

В целом, я заинтересован в поиске «естественных» способов перехода от бесконечного $t$ к циклическому комбинатору, даже если вышеприведенное уравнение не выполняется.

Я также заинтересован в более слабых версиях вышеупомянутого вопроса, например, $t$ может рассматриваться как приложение $t\equiv t_1\ t_2\ldots t_n$ с каждым $t_i$ в нормальной форме (хотя я не уверен, что это действительно помогает).

---

Пока что: естественный подход состоит в том, чтобы использовать $t$ и «перец» приложения $f$ повсюду, например,

$$\Omega:=(\lambda x.x\ x)(\lambda x.x\ x)$$

становится обычным

$$Y_\Omega:= \lambda f.(\lambda x. f\ (x\ x))\ (\lambda x.f\ (x\ x))$$

Идея состоит в том, чтобы свести голову $t$ к лямбда-приложению $\lambda x. t'$ и заменить его на $\lambda x.f\ t'$ , но следующий шаг неясен (и я скептически отношусь к тому, что это может привести ко всему).

Я не уверен, что достаточно разбираюсь в деревьях Бёма, чтобы понять, есть ли у них что сказать, но я сильно сомневаюсь в этом, поскольку дерево Бёма просто ⊥ , которое совсем не похоже на дерево Y Ω : бесконечное дерево абстракции.$\Omega$$\bot$$Y_\Omega$

---

Редактировать : мой друг заметил, что этот наивный подход не работает с термином: Наивный подход даст ( λ x . F ( x x x ) ) ( λ x . f ( x x x ) ) Но это не комбинатор с фиксированной точкой! Это можно исправить, заменив второе приложение f на

$$(\lambda x.x\ x\ x)(\lambda x.x\ x\ x)$$ $$(\lambda x.f\ (x\ x\ x))(\lambda x.f\ (x\ x\ x))$$ $f$ , но тогда f ↦ I не дает первоначального термина. Пока не ясно, является ли этот термин контрпримером к первоначальному вопросу (и, конечно, он не является контрпримером к более общему).$\lambda y z.f\ y$$f\mapsto \mathrm{I}$

В этом очень хорошем вопросе есть несколько аспектов, поэтому я соответствующим образом структурирую этот ответ. $\newcommand{\setof}[1]{\{#1\}}$ $\newcommand{\thra}{\twoheadrightarrow}$ $\newcommand{\codeof}[1]{\lceil #1 \rceil}$

1. Ответ на поставленный вопрос - нет . Термин предложенный вашим другом, действительно является контрпримером.$\Omega_3 = (\lambda x.xxx)(\lambda x.xxx)$

Ранее в комментариях было замечено, что имеются контрпримеры, подобные «огру» , пока вопрос не будет ограничен членами без нормальной нормальной формы слабой головы. Такие термины известны как нулевые термины . Это термины, которые никогда не сводятся к лямбде при любой замене.$K^\infty=Y K$

Для любого комбинатора с фиксированной запятой (fpc) , Y I - это так называемый термин mute (AKA «root-active»): каждый его редукция сводится далее к редексу.$Y$$Y I$

не является немым; также не является Ω 3 - что проявляется в проверке его набора редукций, который равен { Ω 3 ( λ x . x x x ) ⋯ ( λ x . x x x ) ⏟ k ∣ k ∈ N$K^\infty$$\Omega_3$ $-$

$$\setof{\Omega_3 \underbrace{(\lambda x. xxx) \cdots (\lambda x. xxx)}_k \mid k \in \mathbb{N}}$$

Вместо того, чтобы приводить точный аргумент, почему является немым для всех fpcs Y (действительно, для любого циклического комбинатора) - что может быть трудоемким, но, надеюсь, достаточно ясным - я рассмотрю очевидное обобщение вашего вопроса, ограничиваясь также терминами без звука.$Y I$$Y$$-$$-$

Безгласные термины являются подклассом нулевых терминов, которые являются подклассом неразрешимых терминов. Вместе они, пожалуй, являются наиболее популярным выбором для понятия «бессмысленный» или «неопределенный» в лямбда-исчислении, что соответствует тривиальным деревьям Берардуччи, Леви-Лонго и В »соответственно. Решетка понятий бессмысленных терминов был подробно проанализирован Паулой Севери и Фер-Яном де Фрисом. [1] Безгласные термины составляют нижний элемент в этой решетке, т. е. наиболее ограничительное понятие «неопределенный».

2. Пусть будет немым термин, и Y является зацикливание комбинатор со свойством , что Y I = M .$M$$Y$$YI = M$

Во- первых мы утверждаем , что для нового переменного , Y г на самом деле выглядит очень похоже на Y M вы описали, полученный «дождевания г вокруг» некоторый редукта М .$z$$Yz$$Y_M$$z$$M$

По Черч-Россеру, и M имеют общий редуктор, M ′ . Возьмите стандартное сокращение R : Y I ↠ s M ′ . Каждому подтерму в M ′ соответствует единственный подтерм в Y I ≡ Y z [ z : = I ] при этой редукции. Для любого подтерм C [ N ] = M ' , R факторов , как Y I ↠ C $YI$$M$$M'$$R : YI \thra_s M'$$M'$$YI\equiv Yz[z:=I]$$C[N]=M'$$R$ , где средняя нога представляет собой слабое уменьшение головы (а последняя нога является внутренней). N «охраняется» z, если этот второй этап заключает некоторый переопределение I P , а I - потомок замещения [ z : = I ] .$YI \thra C[N_0] \thra_{wh} C[N_1] \thra_i C[N]$$N$$z$$I P$$I$$[z:=I]$

Очевидно, что должен охранять некоторые подтермы M , поскольку в противном случае он также будет отключен. С другой стороны, он должен быть осторожен, чтобы не охранять те подтермы, которые необходимы для не-завершения, поскольку в противном случае он не мог бы развить бесконечное B-омное дерево циклического комбинатора.$Y$$M$

Таким образом, достаточно найти немой термин, в котором каждый подтерм каждого редуктора необходим для ненормализации, в том смысле, что если поместить переменную перед этим подтермом, получится нормализующий термин.

Рассмотрим , где W = λ w . ж я ж ш . Это похоже на Ω , но на каждой итерации мы проверяем, что вхождение W в позиции аргумента не «блокируется» переменной head путем передачи ему идентификатора. Помещение z перед любым подтерием в конечном итоге приведет к нормальной форме z P 1 ⋯ P k , где каждый P i является либо I , W, либо их « z- окраской». Так$\Psi = W W$$W = \lambda w. w I w w$$\Omega$$W$$z$$zP_1\cdots P_k$$P_i$$I$$W$$z$$\Psi$ является контрпримером к обобщенному вопросу.

Теорема. Не существует циклического комбинатора такого, что Y I = Ψ .$Y$$YI = \Psi$

Доказательство. Множество всех редуктов равно { $\Psi$ . Чтобы быть конвертируемым с Ψ , Y я должен привести к одному из них. Аргумент идентичен во всех случаях; для определенности предположимчто Y I ↠ I I W W .$\setof{WW,WIWW,IIIIWW,IIIWW,IIWW,IWW}$$\Psi$$YI$$YI \thra IIWW$

Любое стандартное сокращение может быть пропущено , как Y I ↠ ш P N 4 , Р $YI \thra_s IIWW$

$$\begin{align*} YI \thra_w P N_4, P \thra_w Q N_3, Q \thra_w N_1 N_2, \text{thus } YI \thra_w N_1 N_2 N_3 N_4\\ N_1 \thra I, N_2 \thra I, N_3 \thra W, N_4 \thra W \end{align*}$$

Обратимся к сокращению как R 0 , а сокращения, начиная с N i, как R i .$YI \thra_w N_1 N_2 N_3 N_4$$R_0$$N_i$$R_i$

Эти сокращения могут быть сняты за замену чтобы получить R z 0 : Y z ↠ z k ( М 1 М 2 М 3 М 4 ) N i ≡ M i [ z : = I ], так что R 0 является составом Y I R z 0 [ z : = I ] ↠$[z:=I]$

$$\begin{align*} R^z_0 : Yz \thra z^k(M_1 M_2 M_3 M_4)\\ N_i \equiv M_i[z:=I] \end{align*}$$ $R_0$ .$YI \stackrel{R^z_0[z:=I]}{\thra} I^k(N_1 \cdots N_4) \thra^k_w N_1 \cdots N_4$

$R_i : N_i \thra N \in \setof{I,W}$

$$\begin{align*} R^z_i : M_i \thra N^z_i\\ R_i : N_i \stackrel{R^z_i[z:=I]}{\thra} N^z_i[z:=I] \thra_I N \end{align*}$$

$R_i$$I$$N^z_i[z:=I]$$N$$N^z_i$

$N^z_i$$z$$N$$z$$N$$N \in \setof{I,W}$$N^z_i$

$$\begin{align*} &z^{k_1}(\lambda x. z^{k_2}(x))\\ &z^{k_1}(\lambda w. z^{k_2}( z^{k_3}( z^{k_5}( z^{k_7}(w) z^{k_8}(\lambda x. z^{k_9}(x)) ) z^{k_6}(w) ) z^{k_4}(w) )) \end{align*}$$

So $M_1 M_2 M_3 M_4 \thra N^z_1 N^z_2 N^z_3 N^z_4$, with $N^z_i$ a $z$-sprinkling of $I$ for $i =1,2$ and of $W$ for $i=3,4$.

At the same time, the term $N^z_1 N^z_2 N^z_3 N^z_4$ should yet reduce to yield the infinite fpc Bohm tree $z(z(z(\cdots)))$. So there must exist a "sprinkle" $z^{k_j}$ in one of the $N^z_i$ which comes infinitely often to the head of the term, yet does not block further reductions of it.

And now we are done. By inspecting each $N^z_i$, for $i \le 4$, and each possible value of $k_j$, for $j \le 2+7\lfloor \frac{i-1}{2} \rfloor$, we find that no such sprinkling exists.

For example, if we modify the last $W$ in $IIWW$ as $W^z = \lambda w. z(wIww)$, then we get the normalizing reduction

$$IIWW^z \to I W W^z \to WW^z \to W^z I W^z W^z \to z (I I I I) W^z W^z \thra z I W^z W^z$$

(Notice that $\Omega$ admits such a sprinkling precisely because a certain subterm of it can be "guarded" without affecting non-normalization. The variable comes in head position, but enough redexes remain below.)

3. The "sprinkling transformation" has other uses. For example, by placing $z$ in front of every redex in $M$, we obtain a term $N = \lambda z. M_z$ which is a normal form, yet satisfies the equation $N I = M$. This was used by Statman in [2], for example.

4. Alternatively, if you relax the requirement that $Y I = M$, you can find various (weak) fpcs $Y$ which simulate the reduction of $M$, while outputting a chain of $z$s along the way. I am not sure this would answer your general question, but there are certainly a number of (computable) transformations $M \mapsto Y_M$ which output looping combinators for every mute $M$, in such a way that the reduction graph of $Y_M$ is structurally similar to that of $M$. For example, one can write

$$Y \codeof{M} z = \begin{cases} z (Y \codeof{P[x:=Q]} z) &M\equiv (\lambda x.P)Q\\ Y \codeof{N} z &M \text{ is not a redex and }M \to_{wh} N \end{cases}$$

[1] Severi P., de Vries FJ. (2011) Decomposing the Lattice of Meaningless Sets in the Infinitary Lambda Calculus. In: Beklemishev L.D., de Queiroz R. (eds) Logic, Language, Information and Computation. WoLLIC 2011. Lecture Notes in Computer Science, vol 6642.

[2] Richard Statman. There is no hyperrecurrent S,K combinator. Research Report 91–133, Department of Mathematics, Carnegie Mellon University, Pittsburgh, PA, 1991.