Я пытался написать и проверить компилятор в Agda, используя Конкретную семантику (которая написана для Coq Изабель / HOL) в качестве контрольной точки.Я определяю компиляцию для тех же языков, которые используются в этом тексте.
Для контекста я закончил написание компилятора и сейчас на стадии проверки, однако мне пришлось внести существенную разницу в конкретную семантику в определениивыполнения машинных инструкций.В Agda это различие казалось необходимым, но теперь оно делает этап проверки невероятно сложным.
Пытаясь выполнить более простую версию выполнения инструкций, приведенную в «Конкретной семантике», я натолкнулся на эту строку, которая может объяснить, почемуУ меня возникли проблемы с прямым переводом этого на Агду:
Также полезны заголовок списка, его первый элемент и хвост, остальная часть списка:
fun hd :: 'a list ⇒ 'a
hd (x # xs) = x
Обратите внимание, что, поскольку HOL - это логика полных функций, hd [] определено, но мы не знаем, каков результат. То есть hd [] не является неопределенным, но недоопределенным.
Что означает, что hd [] является недоопределенным?Является ли это эквивалентом наличия неполного шаблона в Agda?
Функция выполнения инструкции сборки в значительной степени зависит от hd.В своей реализации этого в Agda я дал индексы нескольким типам, чтобы позволить мне создавать доказательства того, что в стеке всегда есть минимальное количество элементов, чтобы избежать проблемы неполного сопоставления с образцом.Теперь, когда я пытаюсь проверить компилятор, доказательства являются более сложными, чем доказательства в «Конкретной семантике», поскольку мне приходится работать с этими индексами.
Я что-то упускаю или доказательства в конкретномСемантика неполная с hd [] не определено?