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

Question

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

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

⟦let x = x in x⟧ = ⊥

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

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

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

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

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

Answer 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] (коиндуктивный) самый большой набор S такой, что сорвать x в S, x = [] или же x = (n,ls) с n в Z а также ls в S,

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

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

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

Я считаю, что 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)

РЕДАКТИРОВАТЬ: поскольку "наименьшее" является теоретическим понятием множества, хотя "наименьшее"/"наибольшее" различие может быть неправильным. Определение LF в основном изоморфен GF и является "свободной начальной алгеброй", которая является категорическим формализмом "наименьшей фиксированной точки".

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

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

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

Answer 2

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