Quine в чистом лямбда-исчислении

Я хотел бы привести пример квин в чистом лямбда-исчислении . Я был довольно удивлен, что я не мог найти один, прибегая к помощи. На странице квин есть списки квин для многих «настоящих» языков, но не для лямбда-исчисления.

Конечно, это означает определение того, что я имею в виду под квинем в лямбда-исчислении, которое я делаю ниже. (Я прошу что-то вполне конкретное.)

В некоторых местах, например, Larkin and Stocks (2004), я вижу следующее, цитируемое как «самовоспроизводящееся» выражение: $(\lambda x.x \; x)\;(\lambda x.x \; x)$ . Это сводится к себе после одного шага бета-сокращения, придавая ему ощущение, похожее на quine. Тем не менее, он не похож на quine в том смысле, что он не завершается: дальнейшие бета-сокращения будут продолжать производить то же выражение, поэтому он никогда не приведёт к нормальной форме. Для меня quine - это программа, которая завершает и выводит сама себя, и поэтому я хотел бы получить лямбда-выражение с этим свойством.

Конечно, любое выражение, которое не содержит переопределений, уже находится в нормальной форме и поэтому будет завершаться и выводить себя. Но это слишком тривиально. Поэтому я предлагаю следующее определение в надежде, что оно допустит нетривиальное решение:

определение (предварительное): Квина в лямбда-исчислении - это выражение вида

(λ Икс, A)

$(\lambda x . A)$ (где

A

$A$ обозначает некоторое конкретное выражение для лямбда-исчисления), такое что

((λ x . A) y)

$((\lambda x . A)\,\, y)$ становится

(λ x . A)

$(\lambda x . A)$ или чем-то эквивалентным ему при изменениях имен переменных при уменьшении до нормальной формы длялюбоговвода

y

$y$ .

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

Ссылка

Джеймс Ларкин и Фил Стокс. (2004) "Самовоспроизводящиеся выражения в лямбда-исчислении". Конференции в области исследований и практики в области информационных технологий, 26 (1), 167-173. http://epublications.bond.edu.au/infotech_pubs/158

lambda-calculus Натаниель
источник

Не ответ на мой вопрос, но для моей будущей ссылки (и для будущих посетителей) было бы полезно иметь ссылку на wiki.haskell.org/Combinatory_logic , в которой кто-то имеет более глубокие мысли о квин, чем я.

Натаниэль

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

PyRulez

@PyRulez каков исходный код лямбда-выражения? Если это последовательность символов, то для лямбда-выражения невозможно вывести его, и, следовательно, мы можем определить слово «quine», чтобы означать что-то немного другое для лямбда-выражений, не опасаясь двусмысленности. С другой стороны, если вы думаете о исходном коде как о лямбда-выражении, то «исходный код» и «функция, которую он представляет» - это одно и то же. Так что я думаю, что я в порядке здесь.

Натаниэль

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

PyRulez

Конечно, это не сложно сделать, если вы определите это таким образом. Этот вопрос был о другом.

Натаниэль

Ответы:

Вы хотите термин такой, что : $Q$ $\forall M \in \Lambda$

Q M ⊳_{β} Q

$QM \rhd_\beta Q$

Я не буду указывать никаких дополнительных ограничений на (например, в отношении его формы и того, является ли он нормализующим), и я покажу вам, что он определенно не должен быть нормализующим. $Q$

Предположим , находится в нормальной форме. Выберите (мы можем сделать это, потому что теорема должна выполняться для всех ). Тогда есть три случая. $Q$ $M \equiv x$ $M$
- - некоторый атом . Тогда . Это не сводится к. $Q$ $a$ $QM \equiv ax$ $a$
- является некоторым приложением . Тогда . является нормальной формой по предположению, поэтому также находится в нормальной форме и не сводится к . $Q$ $(RS)$ $QM \equiv (RS)x$ $(RS)$ $(RS)x$ $(RS)$
- - некоторая абстракция (если предполагается свободным в , то для простоты мы можем просто выбрать эквивалентный любой переменной над которой абстрагируется). Тогда . Поскольку находится в нормальной форме, то и $Q$ $(\lambda x.A)$ $x$ $A$ $M$ $\lambda$ $QM \equiv (\lambda x.A)x \rhd_\beta A[x/x] \equiv A$ $(\lambda x.A)$ $A$ , Следовательно, мы не можем привести к . $A$ $(\lambda x.A)$
Поэтому, если такой существует, он не может быть в нормальной форме. $Q$
Для полноты, предположим , что имеет нормальную форму, но не в нормальной форме (возможно , это слабо нормирующий), т.е. с такие , что : $Q$ $\exists N \in \beta\text{-nf}$ $N \not\equiv Q$ $\forall M \in \Lambda$
$Q M ⊳_{β} Q ⊳_{β} N$

Тогда при также должна существовать редукционная последовательность , потому что: $M \equiv x$ $Qx \rhd_\beta Nx \rhd_\beta N$
- возможносчет тогочто . $Qx \rhd_\beta Nx$ $Q \rhd_\beta N$
- должен нормализоваться, поскольку является -nf, а является просто атомом. $Nx$ $N$ $\beta$ $x$
- Если бы нормализовалось ни к чему, кроме , то имеет две nfs, что невозможно по следствию из теоремы Черча-Россера. (Теорема Черча-Россера по существу утверждает, что сокращения, как вы, наверное, уже знаете, слиты). $Nx$ $N$ $Qx$ $\beta$
Но обратите внимание, что невозможно по аргументу (1) выше, поэтому наше предположение о том, что имеет нормальную форму, неверно. $Nx \rhd_\beta N$ $Q$
Если мы допустим такое , то мы уверены, что оно должно быть ненормализующим. В этом случае мы можем просто использовать комбинатор, который исключает любой аргумент, который он получает. Предложение Дениса работает очень хорошо: Тогда только в двух сокращениях: $Q$
$Q \equiv (λ z . (λ x . λ z . (x x)) (λ x . λ z . (x x)))$ $Q \equiv (\lambda z.(λx.λz.(x x)) (λx.λz.(x x)))$ $\beta$ $\begin{aligned} Q M & \equiv (λ z . (λ x . λ z . (x x)) (λ x . λ z . (x x))) M \\ ⊳_{1 β} (λ x . λ z . (x x)) (λ x . λ z . (x x)) \\ ⊳_{1 β} (λ z . ((λ x . λ z . (x x)) (λ x . λ z . (x x))) \\ \equiv Q \end{aligned}$ $\begin{align} QM &\equiv (\lambda z.(λx.λz.(x x)) (λx.λz.(x x))) M \\ & \rhd_{1\beta} (λx.λz.(x x)) (λx.λz.(x x)) \\ & \rhd_{1\beta} (λz.((λx.λz.(x x))(λx.λz.(x x))) \\ & \equiv Q \end{align}$

Этот результат не очень удивителен, так как вы , по сути, просите термин, который исключает любые аргументы, которые он получает, и это то, что я часто упоминаю как прямое применение теоремы о фиксированной точке.

Рой О.
источник

Если бы я мог принять и ответ Дениса, то я бы согласился, но (после того, как я узнал немного больше и смог полностью понять его), именно этот ответ убедил меня в том, что этот «комбинатор квин» не может быть реализован лямбда-выражение в нормальной форме.

Натаниэль

С одной стороны, это невозможно, потому что предполагается, что квинна выводит свой собственный код, а чистое лямбда-исчисление не имеет средств для выполнения вывода.

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

Например, лямбда-член уже является нормальной формой, и, если предположить, что его выходные данные являются результирующей нормальной формой, выходные данные будут . Таким образом, является квине. $(\lambda x. x)$ $(\lambda x. x)$ $(\lambda x. x)$

Дэйв Кларк
источник

Это интересный момент. В этом вопросе я попытался дать определение того, что в лямбда-исчислении может рассматриваться как нетривиальная квинна: функция, которая при применении к любому входному значению бета-сводится к себе (вплоть до подстановки имен переменных). Возможно, это невозможно, но это не очевидно, по крайней мере, для меня.

Натаниэль

Вот предложение:

$A$ $f=\lambda t. (\lambda z.t)$

$Y=\lambda g.((\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x)))$ $A=Y f=(\lambda x.\lambda z.(x\ x))\ (\lambda x.\lambda z.(x\ x))$

$A$ $A$ $\lambda z.A$ $y$ $(\lambda z.A)y \to_\beta A \to_\beta (\lambda z.A)$

Денис
источник

(λ z . A) y

$(\lambda z.A)\;y$

(λ z . A)

$(\lambda z.A)$

A

$A$

y

$y$

y

$y$

y

$y$

A

$A$

(λ z . A) y

$(\lambda z.A)y$

A

$A$

A

$A$

λ z . A

$\lambda z.A$

A

$A$

This behaviour is not very surprising, because thince the "printing" of

λ - c a l c u l u s

$\lambda-calculus$ снова инструкции, quine, печатающий свой собственный код, всегда выполняется. То, что вы спрашиваете, аналогично тому, как запрашивать квинну, чтобы при выполнении вывода ничего не печаталось (что невозможно по определению).

Денис

Ahh, you're right of course. I should have seen that. I'm not sure whether to accept your answer or edit the question to ask for a better definition. I'll give it a bit of thought. (It still seems to me that it should be possible to give a non-trivial definition where you're asking for something that will terminate, but I'm not sure how.)

Nathaniel

Сказав это, правда ли, что

z

$z$ (Я предполагаю, что вы имеете в виду

z

$z$ ) не должен быть свободным в

A

$A$ ? Например

A

$A$ может быть что-то вроде if z==p then return q, otherwise return q. (Псевдокод, потому что я не уверен, возможно ли вообще определить оператор равенства для произвольных выражений в лямбда-исчислении, но я думаю, вы понимаете, о чем я.)

Натаниэль