Ответ 1
ОБНОВЛЕНИЕ: Мое начальное расследование в автобусе сегодня утром было неполным и неправильным. Текст спецификации первой фазы верен. Реализация верна.
Спецификация неверна в том, что на втором этапе порядок событий неверен. Мы должны указывать, что мы делаем вывод выходного типа, прежде чем исправлять независящие параметры.
Человек, этот материал сложный. Я переписал этот раздел спецификации больше раз, чем я помню.Я видел эту проблему раньше, и я отчетливо вспоминаю создание ревизий, так что неверный термин "переменная типа" везде заменялся "параметром типа". (Параметры типа не являются местами хранения, содержимое которых может меняться, поэтому нет смысла называть их переменными.) Я думаю, что в то же время я заметил, что порядок был неправильным. Вероятно, случилось то, что мы случайно отправили более старую версию спецификации в Интернете. Много извинений.
Я буду работать с Mads, чтобы обновить спецификацию в соответствии с реализацией. Я думаю, что правильная формулировка второй фазы должна выглядеть примерно так:
- Если не существует параметров незафиксированного типа, то вывод типа завершается успешно.
- В противном случае, если существует один или несколько аргументов Ei с соответствующий тип параметра Ti такой, что выходной тип Ei с типом Ti содержит по крайней мере один незафиксированный тип параметра Xj и ни один из входных типов Ei с типом Ti не содержит каких-либо незафиксированных тип параметра Xj, то вывод выходного типа производится из всех таких Ei в Ti.
Независимо от того, действительно ли предыдущий шаг сделал вывод, мы должен теперь исправить хотя бы один параметр типа, как показано ниже:
- Если существует один или несколько параметров типа Xi, такие, что Xi нефиксирован и Xi имеет непустое множество оценок и Xi не зависит от любого Xj то каждый такой Xi фиксирован. Если какая-либо операция фиксации не выполняется, вывод типа не выполняется.
- В противном случае, если существует один или несколько параметров типа Xi, такие, что Xi нефиксирован и Xi имеет непустое множество оценок и существует хотя бы один параметр типа Xj, зависящий от Xi то каждый такой Xi фиксирован. Если какая-либо операция фиксации не выполняется, вывод типа не выполняется.
- В противном случае мы не сможем добиться прогресса и незафиксированные параметры. Ошибка ввода типа.
Если вывод типа не терпит неудачу или не выполняется, повторите вторую фазу.
Идея здесь в том, что мы хотим убедиться, что алгоритм никогда не переходит в бесконечный цикл. При каждом повторении второй фазы он либо преуспевает, либо терпит неудачу, либо добивается прогресса. Он не может зацикливаться больше раз, чем есть параметры типа для исправления типов.
Спасибо, что привлек это к моему вниманию.