Квази-котировка - Quasi-quotation

"Quasiquote" перенаправляется сюда. О escape-символе языка программирования, который в некоторых языках программирования называется квазицитатором, см. Обратный апостроф § Использование в программировании.

Квази-цитата или же Цитата Quine это лингвистический прием в формальные языки это способствует строгой и краткой формулировке общих правил языковых выражений при правильном соблюдении использование – упоминание различия. Он был введен философ и логик Уиллард Ван Орман Куайн в его книге Математическая логика, первоначально опубликованный в 1940 году. Проще говоря, квазицитирование позволяет ввести символы, которые стоять за лингвистическое выражение в данном случае и являются используется как это языковое выражение в другом случае.

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

«Снег белый» истинно тогда и только тогда, когда снег белый.
Следовательно, существует некоторая последовательность символов, которая делает следующее предложение истинным, когда каждый экземпляр φ заменяется этой последовательностью символов: «φ» истинно тогда и только тогда, когда φ.

Квази-кавычки используются, чтобы указать (обычно в более сложных формулах), что φ и "φ" в этом предложении связанные с вещи, это один итерация другого в метаязык. Куайн ввел квазиквоты, потому что хотел избежать использования переменных и работать только с закрытые предложения (выражения, не содержащие переменных). Однако ему все еще нужно было уметь говорить о предложениях с произвольным предикаты в них, и, таким образом, квазицитаты предоставили механизм для таких заявлений. Куайн надеялся, что, избегая переменных и схемы, он сводил к минимуму путаницу для читателей, а также оставался ближе к языку, который фактически используют математики.[1]

Квази-кавычки иногда обозначают с помощью символов ⌜ и ⌝ (юникод U + 231C, U + 231D) или двойных квадратных скобок ⟦⟧ («оксфордские скобки») вместо обычных кавычек.[2][3][4]

Как это устроено

Квазикотирование особенно полезно для формулирования правил формирования формальные языки. Предположим, например, что кто-то хочет определить правильные формулы (wffs) нового формального языка, L, с помощью только одной логической операции, отрицание, через следующие рекурсивное определение:

  1. Любые строчные буквы Римская буква (с индексами или без них) - это правильно построенная формула (wff) L.
  2. Если φ - правильная формула (wff) L, то '~ φ' - правильная формула (wff) L.
  3. Ничто иное не является правильной формулой (wff) L.

Правило 2, истолкованное буквально, не выражает очевидного намерения. Для '~ φ' (т. Е. Результат сцепление '~' и 'φ', в таком порядке слева направо) не является правильной формулой (wff) L, потому что нет Греческая буква может встречаться в правильно построенных формулах (wffs) в соответствии с явно предполагаемым значением правил. Другими словами, наше второе правило гласит: «Если некоторая последовательность символов φ (например, последовательность из трех символов φ = '~~п') является правильной формулой (wff) L, то последовательность из двух символов '~ φ' является правильной формулой (wff) L". Правило 2 необходимо изменить, чтобы второе вхождение 'φ' (в кавычках) не воспринималось буквально.

Квазицитирование вводится как сокращение, чтобы уловить тот факт, что формула выражает не совсем цитату, а что-то о конкатенации символов. Наша замена правила 2 с использованием квазицикции выглядит так:

2 '. Если φ - правильная формула (wff) L, то ~ φ⌝ - правильная формула (wff) L.

Квази-кавычки «⌜» и «⌝» интерпретируются следующим образом. Где 'φ' обозначает правильно построенную формулу (wff) L, '⌜ ~ φ⌝' обозначает результат конкатенации '~' и правильная формула (wff), обозначенная 'φ' (в таком порядке слева направо). Таким образом, правило 2 '(в отличие от правила 2) влечет за собой, например, что если 'п'- правильная формула (wff) L, затем '~п'- правильная формула (wff) L.

Точно так же мы не могли определить язык с дизъюнкция добавив это правило:

2.5. Если φ и ψ - правильные формулы (wffs) L, то '(φ v ψ)' - правильная формула (wff) L.

Но вместо:

2,5 '. Если φ и ψ - правильные формулы (wffs) L, то (φ v ψ) ⌝ - правильная формула (wff) L.

Квази-кавычки здесь интерпретируются точно так же. Где 'φ' и 'ψ' обозначают правильные формулы (wffs) L, '⌜ (φ v ψ) ⌝' обозначает результат конкатенации левой скобки, правильную формулу (wff), обозначаемую 'φ', пробел, 'v', пробел, правильную формулу (wff), обозначаемую как 'ψ' и правая скобка (в указанном порядке слева направо). Как и раньше, правило 2.5 '(в отличие от правила 2.5) влечет, например, что если'п' и 'q'являются правильными формулами (wffs) L, тогда '(п v q) 'является правильной формулой (wff) L.

Предупреждение

Нет смысла проводить количественную оценку в квазицитированных контекстах, используя переменные которые охватывают другие вещи, кроме строки символов (например. числа, люди, электроны ). Предположим, например, что кто-то хочет выразить идею, что 's(0) 'обозначает преемника 0,'s(1) 'обозначает преемника 1 и т. Д. Кто-то может сказать:

Предположим, например, φ = 7. Что такое ⌜s(φ) ⌝ в этом случае? Все следующие предварительные интерпретации были бы одинаково абсурдными:

  1. ⌜s(φ) ⌝ = 's (7)',
  2. ⌜s(φ) ⌝ = 's (111)' (в двоичной системе 111 означает целое число 7),
  3. ⌜s(φ) ⌝ = 's (VII)',
  4. ⌜s(φ) ⌝ = 's (семь)',
  5. ⌜s(φ) ⌝ = 's (семь)' (семь по-русски означает семь),
  6. ⌜s(φ) ⌝ = 's (количество дней в неделе)'.

С другой стороны, если φ = '7', тогда ⌜s(φ) ⌝ = 's (7)', а если φ = 'семь', тогда ⌜s(φ) ⌝ = 's (семь)'.

Расширенная версия этого заявления гласит:

  • Если φ является натуральным числом, тогда результат конкатенации 's', левая скобка, φ, а правая скобка (в этом порядке слева направо) обозначает преемника φ.

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

Правильный способ сформулировать принцип:

  • Если φ является Арабская цифра который обозначает натуральное число, то ⌜s(φ) ⌝ обозначает последователя числа, обозначаемого φ.

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

Пока эти соображения приняты во внимание, совершенно безвредно «злоупотреблять» обозначением угловой цитаты и просто использовать ее всякий раз, когда требуется что-то вроде цитаты, но обычная цитата явно не подходит.

Смотрите также

Рекомендации

  1. ^ Предисловие к пересмотренному изданию 1981 г.
  2. ^ "Что такое денотационная семантика и для чего она нужна?".
  3. ^ Даути Д., Уолл Р. и Питерс С .: 1981, Введение в семантику Монтегю, Springer.
  4. ^ Скотт, Д. и Стрейчи, С .: 1971, К математической семантике компьютерных языков, Вычислительная лаборатория Оксфордского университета, Исследовательская группа по программированию.
  • Куайн, В. В. (2003) [1940]. Математическая логика (Пересмотренная ред.). Кембридж, Массачусетс: Издательство Гарвардского университета. ISBN  0-674-55451-5. Cite имеет пустые неизвестные параметры: | месяц = и | соавторы = (помощь)

внешняя ссылка