Мартин-Лёф о наборах и рядах альтернатив
Выкладываю видеозапись выступления П. Мартин-Лёфа на конференции в Питере 24 июня 2010. К сожалению, не вся лекция заснята - аккумулятор сел под конец :(
Честно говоря, я мало что понял, особенно в конце. Там не только топологию и теорию множеств, но еще теорию категорий надо разуметь... Но сама постановка проблемы мне кажется интересной - в той мере, в какой он предлагает переосмыслить семантику возможных миров.
(не уверен, что перевел все правильно - но в официальном хэндауте перевод, по-моему, вообще оставляет желать лучшего):
"В моей статье "Математика бесконечности" (1990) конструктивная теория типов была расширена добавлением аксиом, регламентирующих понятие единичной последовательности выборов (single choice sequence). Получившееся нестандартное расширение теории типов имеет в качестве своей естественной интерпретации индуктивный, или прямой предел комма-моделей (?) (comma models) теории типов, где под комма-моделью я понимаю стандартную модель на некотором лежащем в основе пространстве исходов (sample space) в смысле теории вероятностей. Эта модель является нестандартной моделью стандартной теории типов, но должна рассматриваться как стандартная модель, или намеренная (intended) интерпретация, нестандартного расширения теории типов, упомянутого выше. С тех пор прошло двадцать лет, но основная проблема осталась прежней: как расширить теорию типов, добавляя не только единичные последовательности выборов (single choice sequences), но и целые наборы последовательностей выборов (spreads of choice sequences). Это необходимо, если теория наборов и последовательностей выборов должна стать частью теории типов.
То же самой можно выразить и в терминах возможных миров. Как объяснил Ранта (1993,1994), последовательность выборов можно трактовать как возможный мир в «в состоянии рождения» (statu nascendi). Другими словами, на любом конкретном этапе детерминирован только финитный начальный ее сегмент, будущее же ее развитие является пока недетерминированным. В терминах возможных миров, добавление не только единичных последовательностей выборов, но и целых наборов, предполагает расширение теории типов с помощью аксиом для всего спектра возможных миров, а не только для единственного возможного мира, как в случае с обычной (?) (full-scale) семантикой возможных миров. На самом деле, если пренебречь различиями в словесном выражении, все сводится к проблеме включения аппарата семантики возможных миров в конструктивную теорию типов."
Честно говоря, я мало что понял, особенно в конце. Там не только топологию и теорию множеств, но еще теорию категорий надо разуметь... Но сама постановка проблемы мне кажется интересной - в той мере, в какой он предлагает переосмыслить семантику возможных миров.
You can watch this video on www.livejournal.com
(не уверен, что перевел все правильно - но в официальном хэндауте перевод, по-моему, вообще оставляет желать лучшего):
"В моей статье "Математика бесконечности" (1990) конструктивная теория типов была расширена добавлением аксиом, регламентирующих понятие единичной последовательности выборов (single choice sequence). Получившееся нестандартное расширение теории типов имеет в качестве своей естественной интерпретации индуктивный, или прямой предел комма-моделей (?) (comma models) теории типов, где под комма-моделью я понимаю стандартную модель на некотором лежащем в основе пространстве исходов (sample space) в смысле теории вероятностей. Эта модель является нестандартной моделью стандартной теории типов, но должна рассматриваться как стандартная модель, или намеренная (intended) интерпретация, нестандартного расширения теории типов, упомянутого выше. С тех пор прошло двадцать лет, но основная проблема осталась прежней: как расширить теорию типов, добавляя не только единичные последовательности выборов (single choice sequences), но и целые наборы последовательностей выборов (spreads of choice sequences). Это необходимо, если теория наборов и последовательностей выборов должна стать частью теории типов.
То же самой можно выразить и в терминах возможных миров. Как объяснил Ранта (1993,1994), последовательность выборов можно трактовать как возможный мир в «в состоянии рождения» (statu nascendi). Другими словами, на любом конкретном этапе детерминирован только финитный начальный ее сегмент, будущее же ее развитие является пока недетерминированным. В терминах возможных миров, добавление не только единичных последовательностей выборов, но и целых наборов, предполагает расширение теории типов с помощью аксиом для всего спектра возможных миров, а не только для единственного возможного мира, как в случае с обычной (?) (full-scale) семантикой возможных миров. На самом деле, если пренебречь различиями в словесном выражении, все сводится к проблеме включения аппарата семантики возможных миров в конструктивную теорию типов."