из Митчелла, про Y-комбинатор

[deni_ok]

Отличное упражнение на свойства комбинатора неподвижной точки fix.

Докажите равенство

fix (f . g) = f (fix (g . f))

Comments

[ext_4199]

Это равенство, между прочим, лежит в основе worker/wrapper transformation.

[deni_ok]

Ага, спасибо, worker/wrapper - хорошая идея. Оно (равенство), оказывается, имеет подходящее название - rolling rule.

[ext_4199]

Вообще, хорошо бы указать, в какой формальной системе это надо доказывать :)

В частности, Митчелл вводит важное правило, с которым это делается легко, а без которого (то есть используя только аксиому fix f = f (fix f)) фиг докажешь.

Правило выглядит так: если M ->> N M, то M = fix N.

[kurilka]

а "Митчелл" в данном случае это что?

[ext_4199]

http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=3460

[kurilka]

Думаю скорее http://www.rsdn.ru/res/book/prog/FoundationsForPL.xml :)
У меня так всё руки пока не доходят...

[migmit]

(f . g) (f (fix (g . f))) = f (g (f (fix (g . f))) = f ((g . f) (fix (g . f))) = f (fix (g . f)). Так как fix - минимальная неподвижная точка, получаем, что fix (f . g) <= f (fix (g . f)).

Аналогично, fig (g . f) <= g (fix (f . g)). Так как f - морфизм доменов, получаем, что f (fix g . f) <= f (g (fix (f . g))) = (f . g) (fix (f . g)) = fix (f . g). Два неравенства вместе дают нужное равенство.

[ext_4199]

Строго говоря, ты доказал, что [[fix (f . g)]] = [[f (fix (g . f))]], т.е. что они эквивалентны денотационно. После этого должна идти апелляция к полноте подразумеваемой proof system по отношению к этой денотационной семантике. Которая вряд ли имеет место.

[migmit]

Я человек простой, f от [[f]] не отличаю.

> Которая вряд ли имеет место.

А почему, кстати?

[ext_4199]

Вроде как здесь http://www.pps.jussieu.fr/~berline/BMS08.pdf доказано, что теория, порожденная семантикой Скотта, не является рекурсивно перечислимой.