lambda x.x x - ?

[arseniiv]

Sonic86 в сообщении #1155139 писал(а):

А как же:

Sonic86 в сообщении #1154931 писал(а):

бывают функции (функционалы?), которые можно вычислять от самих себя: например, если $g(f) = f\circ f \circ f$, то $g(g)=g^{(9)}$ - $9$-ирная композиция $g$

Чтобы провернуть подобное в ZFC с обычными функциями, придётся или избавиться от аксиомы регулярности, или использовать какое-то отображение, переводящее $g$ не в $g$. Но вот если рассматривать аппликацию $fa$ не как применение обычной функции $f$ к аргументу, а как применение функции с кодом $f$, то, правда, мы в результате и получим что-то типа λ- или комбинаторного исчисления — надо будет только потребовать, чтобы аргументы и результаты задавались такими же кодами, а раз нам нужно $gg$, это самый простой выход.

[Eimrine]

(Оффтоп)

Sonic86 в сообщении #1155095 писал(а):

Пока Харрисона читаю.

А это кто? Гугл мне только актёров да музыкантов подсовывает.

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

[Sonic86]

Eimrine в сообщении #1155162 писал(а):

А это кто? Гугл мне только актёров да музыкантов подсовывает.

В Вики упомянут учебник по ФП: https://ru.wikipedia.org/wiki/%D0%A4%D1 ... 0%B8%D0%B5
у меня их аж 3.

arseniiv в сообщении #1155152 писал(а):

Чтобы провернуть подобное в ZFC с обычными функциями, придётся или избавиться от аксиомы регулярности, или использовать какое-то отображение, переводящее $g$ не в $g$. Но вот если рассматривать аппликацию $fa$ не как применение обычной функции $f$ к аргументу, а как применение функции с кодом $f$, то, правда, мы в результате и получим что-то типа λ- или комбинаторного исчисления — надо будет только потребовать, чтобы аргументы и результаты задавались такими же кодами, а раз нам нужно $gg$, это самый простой выход.

Странно немного. Ладно, вечером почитаю...

[arseniiv]

Не, я наврал, Барендрегт во введении сам пишет, что не рассматривает просто типизированное. Про него есть только в приложении A.

[Munin]

Sonic86 в сообщении #1155139 писал(а):

Тут понятно: 1-е - это что-то типа $\mathrm{Apply}$ - берет функцию и аргумент и применяет одно к другому. Правда странно, но 2-й терм, $\alpha$-равносильный первому вызывает вообще другие ассоциации - композиция функций.

Да, вот именно. С этим надо разобраться. То есть, в выражении $f\, x$ аргумент $x$ сам вполне может оказаться функцией (или чем-то похуже - функтором и т. д.), и тогда простое применение превращается в композицию функций. Поскольку для $\lambda$-исчисления это одно и то же, то вы видите, насколько сложно здесь представлять функцию графиком. Здешние "функции" определены на слишком сложном и широком множестве.

Зато если представлять себе функцию как алгоритм вычисления, то получается понятно. $f\,x$ - это вычисление функции $f$ при аргументе $x.$ Дальше, $f\,g\,x$ - это вычисление композиции функций $f\circ g$ при том же аргументе. Казалось бы! Но на самом деле, аппликация левоассоциативна, так что $f\,g\,x=(f\,g)\,x$ а не $f\,(g\,x).$ Если $f$ здесь - какая-то обычная вычислительная функция, например, $f=\lambda x.x^2+2\cdot x+2,$ то всё будет окей, это будет композиция. А если $f$ - какое-нибудь безобразие? Например, простейшая каррированная функция $\lambda ab.b.$ Она уже не будет подходить под понятие "композиции": применяя её последовательно к $g\,x,$ мы получим $x,$ какой бы ни была $g$! Даже если $g$ будет константой, теряющей всю информацию об аргументе.

Sonic86 в сообщении #1155139 писал(а):

Соответственно - мой вопрос - это функция, которая применяется сама к себе, причем она переменная. Что-то такое.

Не торопитесь, скурите сначала предыдущий абзац. А потом будет проще: ваша функция - это просто $(\lambda fa.f\,a)\,x\,x.$

[Sonic86]

Munin в сообщении #1155204 писал(а):

Да, вот именно. С этим надо разобраться. То есть, в выражении $f\, x$ аргумент $x$ сам вполне может оказаться функцией (или чем-то похуже - функтором и т. д.), и тогда простое применение превращается в композицию функций. Поскольку для $\lambda$-исчисления это одно и то же, то вы видите, насколько сложно здесь представлять функцию графиком. Здешние "функции" определены на слишком сложном и широком множестве.

Еще пришла в голову такая мысль: можно $x$ понимать как функцию, которая везде тождественно равна $x$, тогда расхождение исчезает.

[Munin]

Да! Yes, yes, yesssss!!!

Но тогда вы внезапно оказываетесь в мире, в котором нет ничего, кроме функций. Впрочем, это и есть мир $\lambda$-исчисления.

[arseniiv]

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

Короче говоря, функция нуля аргументов как частный случай функции $n$ аргументов — это must. Но такая же функция вдобавок к функциям единственного аргумента — это уже не айс.

-- Ср сен 28, 2016 17:37:33 --

Хотя если вспомнить, кто такая функция $n$ аргументов с точки зрения теории множеств, картины сходятся. Функция 0 аргументов тогда будет функцией одного аргумента, берущегося из нулевой декартовой степени чего-нибудь, которая всегда состоит из одного пустого кортежа.

-- Ср сен 28, 2016 17:38:18 --

(Я что-то не очень связное написал — теперь, как будто, уже неясно, в чём point.)

-- Ср сен 28, 2016 17:45:19 --

Вообще говоря, проблема другая: если назвать все значения функциями нуля аргументов, получится круг в определении, который устранится только если мы станем называть функциями что-то особое. Ну, например, действительно, какой смысл называть комбинатор $\Omega\equiv(\lambda x.xx)(\lambda x.xx)$ функцией?

[Munin]

Ну да. Меня с самого начала тянуло написать не

...нет ничего, кроме функций...

а

...нет ничего, кроме "функций"...

Потому что "функция", которая зацикливается в своём вычислении, и никогда не выдаёт результата, - это не функция. Но такие в функциональных языках есть и даже используются.