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

[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]

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