S K I in Forth

[juan_gandhi]

http://soton.mpeforth.com/flag/jfar/vol4/no4/article6.pdf

But my bigger question is: can anybody direct me to a good definition of J combinator? Somebody mentioned recently, I forgot who. Now I'm stuck.

Comments

[romanovsky.livejournal.com]

Ищется ловчее, коли его "J operator" обозвать.

[spamsink.livejournal.com]

КМК, использование буквы J для оператора имени Питера Лэндина и для комбинатора имени Мозеса Шёнфинкеля - это омонимия. Про комбинатор тут: http://www.wolframscience.com/nksonline/page-1123a-text

[sergeif.livejournal.com]

О как. Интересно, есть какая-нибудь польза от него?

Я думал речь про Jxyzw -> xy(xwz), про которого известны ограничения на длину редукции в базисе J I. (http://home.inf.unibe.ch/~tstuder/papers/j.pdf)

[spamsink.livejournal.com]

Сооответственно, этот J имени Россера не может давать JJ=S. Что ж такое с этим J, будто математикам там джемом намазано?

[sergeif.livejournal.com]

В Haskell'евской комбинаторной либе jay имени Rosser'а. И в литературе по комбинаторам тоже часто бывает. И правда, любят математики (от CS?) букву J.

[spamsink.livejournal.com]

Польза от J-Landin или от J-Schoenfinkel?

[sergeif.livejournal.com]

От J-Schoenfinkel. Короткий кусок по ссылке я осознал не вполне. Идея в том, что терм, состоящий из комбинаторов без переменных может быть представлен как бинарное дерево довольно забавная, да, но ничего извлечь из нее я не умею. Способ перечислить комбинаторы?

[spamsink.livejournal.com]

Это упрощает представление. В SK(I) нужно в дереве хранить тип комбинатора, а в J - не нужно, потому что он всего один.

[sergeif.livejournal.com]

В случае с J про дерево я понимаю, оно возникает из-за того, что сам J можно опустить и оставить только скобки (()(()())), которые эквивалентны бинарному дереву. А что за дерево для SKI? Имеется в виду уже не бинарное, а просто дерево, где в листьях переменные, а в узлах комбинаторы?

[pbl.livejournal.com]

> А что за дерево для SKI? Имеется в виду уже не бинарное, а просто дерево, где в листьях переменные, а в узлах комбинаторы?

Абстракция не нужна, это же суть комбинаторной логики. Все равно бинарное дерево со значениями в листьях. Либо приложение двух выражений, либо комбинатор. Фикспойнт X. A + X * X, только для базиса J A = 1, для SK A = 2, для SKI A = 3.

[sergeif.livejournal.com]

Про дерево понял, про фикспойнт не понял. Что такое A+X*X?

[pbl.livejournal.com]

В хаскелевской нотации, например, newtype F a x = F (Either a (x, x)). Тип бинарных деревьев есть неподвижная точка этого функтора (по x). Синтаксическое дерево выражений комбинаторной логики для J-базиса изоморфно Fix (F ()), SK - Fix (F Bool) etc.

[sergeif.livejournal.com]

Ок, это кажется изящным, но не естественным для меня. То есть A -- это множество равносильное множеству базисных комбинаторов, Fix чтобы избавиться от рекурсии в определении синтаксического дерева комбинаторов через CAST = A | App CAST CAST. Either просто чтобы выразить сумму в этом типе. Так?

[pbl.livejournal.com]

> То есть A -- это множество равносильное множеству базисных комбинаторов

Да, именно так.

> Fix чтобы избавиться от рекурсии в определении синтаксического дерева комбинаторов

Это я вообще рефлекторно, извините, привык в последнее время думать об индуктивных типах в таких терминах, здесь это нахрен не нужно. Да, все как вы пишете.

[sergeif.livejournal.com]

Ага, спасибо. Ну, мне было интересно. )

[juan-gandhi.livejournal.com]

Спасибо за ваш коммент выше. Красиво, ясно и логично, на самом деле. И как бы намечает мост к типизированной лямбде.

[pbl.livejournal.com]

Ну там без HOAS на практике не обойтись, мне тут как раз недавно довелось поломать голову на эту тему на работе, как ни странно.

> Красиво, ясно и логично, на самом деле.

Но устарело же. Сейчас in vogue делать то же самое через свободные монады.

[zeit-raffer.livejournal.com]

у меня оффтопик-вопрос.

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

[pbl.livejournal.com]

У меня плохо получалось заинтересовать даже более простыми и доступными темами. Причем специально отобранных мною же нетупых студентов. Так что... без внутренней мотивации я не думаю, что это стоит потраченного времени. Ну и вообще это такой интересный путь, который надо с квикчека проходить. Вот когда уже квикчек в продакшне проверяет пропертиз, и ни у кого это не вызывает больших вопросов, можно начинать говорить: "А ПРИКИНЬТЕ, ТО ЖЕ САМОЕ МОЖНО ДОКАЗЫВАТЬ!"

[zeit-raffer.livejournal.com]

тут интересный вопрос, откуда берется мотивация такого рода... но не буду, не буду.

[pbl.livejournal.com]

У меня - от двадцати лет в траншеях. Но некоторых устраивает каждый день лопатовать одно и то же говно безо всякого проблеска и надежды. Чо, бапки капают, мухи не кусают. Лафа.

[juan-gandhi.livejournal.com]

Только не множество. Теория множеств тут не пришей не пристегни.

[sergeif.livejournal.com]

Было бы интересно услышать правильную формулировку о связи базисных комбинаторов и типа A.

[pbl.livejournal.com]

Просто с точки зрения чистой теории типов, множества ли типы или нет - совершенно несущественно. Можно изобретать всякие комбинаторные алгебры, моделирующие разные исчисления, рядом с которыми ZFC и проч. рядом не валялись. Весьма доставляют методы искоренения абстракции изложенные в чисто категорных терминах (для разных значений доставлючести в зависимости от личных предпочтений и испорченности). Но это за пределами моего понимания. А так-то, ежели по-простому, по-черчевски, то ну как бы множества, да.

[sergeif.livejournal.com]

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

[spamsink.livejournal.com]

Переменных там нет, а в узлах комбинаторы, да.

[pappadeux.livejournal.com]

оно связанон как-то с iota combinator?

[spamsink.livejournal.com]

Разве что тем, что оба дают базис из одного комбинатора, но J дает более короткое представление, а у iota более простое определение.