Являются ли денотационные семантические сопоставления разрешимыми?

Извиняюсь за мое плохое выражение этого вопроса, я не уверен, что у меня есть словарь, чтобы спросить его соответствующим образом.

Я написал (совсем недавно) нечто похожее на

⟦let x = x in x⟧ = ⊥

но на самом деле я не понимаю здесь ничего сложного. Я могу утверждать, что это утверждение действительно ⊥, потому что я знаю, что это непроизводительный бесконечный цикл. Кроме того, я могу утверждать что-то вроде

⟦let ones = 1:ones in ones⟧ = μ(λx.(1,x)) = (1, (1, (1, ... )))

но что входит в этот элипсис? Предположительно, это бесконечное количество "1-и-кортежей", прекрасно определенный математический объект, если вы в порядке с AFA, но как я могу убедить вас, что это не какое-то конечное число "1-и-кортежей", а затем непроизводительный ⊥?

Очевидно, что это связано с ответом на проблему остановки, поэтому я вообще не могу.

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

Ответ 1

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

Я не думаю, что это проблема.

Существует различие между индуктивными и коиндуктивными определениями. Теоретически мы можем исследовать этот набор:

Индуктивное определение списка целых чисел:

набор [Z] - это наименьший набор S, так что пустой список находится в S и такой, что для любого ls в S и n в Z пара (n,ls) в S.

Это также может быть представлено в виде "ступенчатого индексирования" как [Z](0) = {[]} и [Z](n) = {(n,ls) | n \in Z, ls \in [Z](n-1)}, который позволяет определить [Z] = \Union_{i \in N}([Z](n) (если вы верите в натуральные числа!)

С другой стороны, "списки" в Haskell более тесно связаны с "коиндуктивными потоками", которые определяются коиндуктивно

множество [Z] (coinductive) является наибольшим набором S таким, что forall x в S, x = [] или x = (n,ls) с n в Z и ls в S.

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

Нетрудно показать, что все индуктивные списки имеют конечную длину, а некоторые коиндуктивные списки бесконечно велики. Ваш пример требует coinduction.

В более общем случае индуктивные определения могут быть хотя бы "наименее фиксированной точкой функтора", в то время как коиндуктивные определения можно рассматривать как "наибольшую фиксированную точку функтора". "Наименее фиксированная точка" функтора является его "исходной алгеброй", а "наибольшая фиксированная точка" - его "конечная коалгебра". Использование этого в качестве семантических инструментов облегчает определение вещей в категориях, отличных от категории множеств.

Я нахожу, что Haskell предоставляет хороший язык для описания этих функторов

data ListGenerator a r = Cons a r | Nil

instance Functor (ListGenerator a) where
  fmap f (Cons a x) = Cons a (f x)
  fmap _ Nil        = Nil

хотя haskell предоставляет хороший язык для описания этих функторов, поскольку его функциональное пространство CBN, а язык не является полным, у нас нет способа определить наименьшую точку исправления, которую мы хотели бы:(, хотя мы получаем определение наибольшей фиксированной точки

data GF f = GF (f (GF f))

или нерекурсивный экзистенциально квантифицированный

data GF f = forall r. GF r (r -> (f r))

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

data LF f = LF (forall r. (f r -> r) -> r)

EDIT: поскольку "наименьшее" представляет собой теоретико-множественное множество, хотя "наименьшее" / "наибольшее" различие может быть не правильным. Определение LF в основном изоморфно GF и является "свободной начальной алгеброй", которая является категорическим формализмом "наименее фиксированной точки".

относительно

как я могу убедить вас, что это не какое-то конечное число "1-и-кортежей", а затем непроизводительное ⊥?

вы не можете, если я не верю в конструкции в этом посте. Если да, то ваше определение оставляет меня застрявшим!. Если вы скажете: "ones - коиндуктивный поток, состоящий из пары (1,ones)", тогда я должен поверить! Я знаю, что ones по определению не _|_, и, следовательно, по индукции я могу показать, что это не может быть так, что для любого значения n у меня есть n единицы, а затем снизу. Я могу попытаться опровергнуть ваше утверждение только отрицанием существования коиндуктивных паров.

Ответ 2

Более подробно о методах доказательства над коиндуктивными структурами (расширяя на Филиппа JF очень хороший ответ), вы можете взглянуть на Хинце и Джеймса "Доказательство правильности принципа фиксированной точки": http://www.cs.ox.ac.uk/people/daniel.james/unique/unique-tech.pdf