Mazdaywik commented 6 years ago

Нужно добавить во входной язык (в оба) условия-отрицания, т.е. условия, в которых сопоставление с образцом не должно выполняться.

Мотивация

Иногда очень не хватает отрицательных условий. Иногда приходится явно перечислять образцы-исключения, дабы отсечь варианты. Иногда приходится писать неуклюжие условия вида , <Equal s.1 s.2> : False, потому что по-другому выражать неравенства ещё хуже. Это как удлинение e-переменных справа-налево. Нужно очень редко, но когда нужно — обидно, что его нет.

Другая причина. Оптимизации #122 и #126 могли бы работать с простыми отрицательными условиями — классическими рестрикциями Турчина (s.1 ≠ X, s.1 ≠ s.2, e.1 ≠ ε), например, отсекать недостижимые предложения. Альтернатива — усложнение оптимизаторов для неявного учёта отрицательной информации из предыдущих предложений.

Третья причина. На Рефале-5λ сможет быть выражен результат суперкомпиляции, рестрикции будут записываться при помощи отрицаний.

Обзор других диалектов

Рефал Плюс

В Рефале Плюс можно использовать отрицания условия. Синтаксически они выглядят так:

ОтрицаниеУсловия = "#" Источник [Хвост]

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

Рефал-6

Рефал-6 позволяет в начало любого действия поставить знак #, который инвертирует неуспех в нём — неуспех заменяется на пустое выражение, отсутствие неуспеха приводит к неуспеху.

Предлагаемый синтаксис

Рефал-5λ

В условиях и присваиваниях можно заменить знак : на знак # — сопоставление с образцом должно не выполняться:

, Res # Pat
= Res # Pat

Область видимости переменных в отрицаемом образце ограничена самим этим образцом. Если образец содержит переопределяемые переменные, то значения одноимённых переменных в последующей части предложения не меняются.

Отрицательное присваивание является синтаксическим сахаром. Запись

= Res # Pat

эквивалентна

= : , Res # Pat

Т.е. отрицательное присваивание при успешном сопоставлении валит программу.

Простой Рефал

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

Поэтому отрицательные условия будут выглядеть так:

! Res : Pat

Возможная реализация

Обычное условие компилируется в такой код:

F {
  Pat, ResC : PatC = Res;
  . . .
}

(CmdSentence
  сопоставление с Pat
  построение <F?1 ResC>
  (CmdSentence
    сопоставление с <F?1 PatC>
    построение Res
    (CmdNextStep)
  )
  удаление <F?1 . . .>
)
. . .

Отрицания будут компилироваться так:

F {
  Pat, ResN # PatN = Res;
  . . .
}

(CmdSentence
  сопоставление с Pat
  построение <F!1 ResN>
  NEG = FALSE
  (CmdSentence
    сопоставление с <F!1 PatN>
    NEG = TRUE
  )
  удаление <F!1 . . .>
  if NEG then FAIL
  построение Res
)
. . .

Т.е. потребуются три новые команды языка сборки и флаг NEG. Можно даже обойтись одной командой, используя разные её аргументы.

Обсуждение в рассылке refal@botik.ru

Mazdaywik commented 5 years ago

Аргумент от @InfiniteDisorder в пользу отрицательных условий:

https://github.com/bmstu-iu9/refal-5-lambda/blob/4ed95a0af96abfda5654ba8e4c7bf9ad680c4427/src/compiler/OptTree-Drive.ref#L254-L266

Очевидно, t.Res # None было бы нагляднее, проще и эффективнее.

Mazdaywik commented 4 years ago

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

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

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

Mazdaywik commented 4 years ago

Интересный вопрос — как отрицания будут взаимодействовать с прогонкой (#248).

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

Отрицание тоже является клэшем, только результаты его решения нужно интерпретировать иначе. Если решение есть и однозначное, то значит отрицание никогда не выполняется — стираем предложение. В остальных случаях проще всего оставлять отрицание неизменным. При неопределённом решении ничего не делаем по определению. В случае решения с сужениями — правильнее генерировать помимо набора сужений ещё и набор отрицательных сужений и их применять в случае отрицания. Но это не всегда возможно в случае Рефала-5λ: s-переменная и выражение в круглых скобках не образуют в сумме t-переменной, поскольку есть неопределённое количество различных АТД-термов.

Кроме того, решением отрицаний могут быть классические рестрикции Рефала. Их можно привязывать к образцам и затем учитывать при прогонке.

Mazdaywik commented 3 years ago

В дополнение к предыдущему комментарию. Отрицательное условие можно считать синтаксическим сахаром:

, Res # Pat

эквивалентно

, Res : { Pat = True; e._ = False } : False

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

В принципе, с точки зрения прогонщика вполне законно раскрывать отрицание как этот синтаксический сахар и в этом ключе прогонять. В частности, для ситуаций невыполнения отрицания вызывать функции-продолжения <Func*〈n+1〉 …> следующих предложений.

Mazdaywik commented 3 years ago

В частности, для ситуаций невыполнения отрицания вызывать функции-продолжения <Func*〈n+1〉 …> следующих предложений.

Речь идёт о том, что отрицания интерпретировать примерно так:

F {
  . . .
  P, R′ # P′ = R;  /* предложение номер k */
  . . .
}
↓ ↓ ↓
F {
  . . .
  P, R′ : P′ = <F*〈k+1〉 P>;
  P = R;
  . . .
}

Вроде должно работать правильно.

А вообще, реализовывать условия-отрицания можно в два этапа:

Как синтаксический сахар, описанный выше
```
, Res : { Pat = True; e._ = False } : False
```
Нормальная нативная низкоуровневая реализация.

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

Pat ! Res′ : Pat′ = Res

изначально предложенный для Простого Рефала? Хотя синтаксис , Pat # Res нагляднее.

bmstu-iu9 / refal-5-lambda

Условия-отрицания #168