Brouwer’s Cambridge Lectures on Intuitionism (1981)
The First Act of Intuitionism. The complete separation of mathematics from mathematical language, and hence from the linguistic phenomena which are described by theoretical logic, the recognition that intuitionistic mathematics is an essentially languageless activity of the mind which springs from the perception of a motion of time. This perception of time can be described as the splitting of a life moment into two distinct things, one of which gives place to the other, but is preserved in memory. If the dyad thus born is stripped of every quality, what remains is the blank form of the common substratum of all dyads. And it is this common substratum, this common form, which is the basic intuition of mathematics.
https://www.cs.kent.ac.uk/people/staff/dat/tfp12/tfp12.pdf Turner, "Some History of Functional Programming Languages"
Оказывается SASL это "St Andrews Static Language"
Оказывается SASL это "St Andrews Static Language"
Всего неделю пользуюсь вертикальной мышкой, и уже при попытке пересаживания за классическую довольно быстро ощущается какое-то легкое напряжение в разгибателях предплечья. Впрочем, возможно это самовнушение.
TIL что частичные коммутативные моноиды, именуемые логиками separation algebra, в квантмехе обзывают https://ncatlab.org/nlab/show/effect+algebra
https://arxiv.org/abs/1708.02143 Litak, Visser, "Lewis meets Brouwer: constructive strict implication"
Известно, что монадические и комонадические исчисления соответствуют по Карри-Говарду модальным логикам с унарной модальностью □, а как насчёт стрелок Хьюза? Оказывается, им соответствует двухместная модальность ⥽, так называемая "строгая импликация". Более того, изначальная формулировка модальной логики по Льюису вводила именно строгую импликацию как первичный конструкт, а □ выражалась через неё. После ряда работ Гёделя стрелку забыли в пользу коробки, в том числе потому, что в классическом варианте эти модальности взаимовыразимы. Как водится, в конструктивной формулировке симметрия распадается на независимые сущности, имеющие разные семантики - добавляя к строгим импликациям дополнительные схемы, можно получить логику для стрелок или любимой тотальщиками guarded recursion (кстати, как по русски - охраняемая рекурсия?).
Известно, что монадические и комонадические исчисления соответствуют по Карри-Говарду модальным логикам с унарной модальностью □, а как насчёт стрелок Хьюза? Оказывается, им соответствует двухместная модальность ⥽, так называемая "строгая импликация". Более того, изначальная формулировка модальной логики по Льюису вводила именно строгую импликацию как первичный конструкт, а □ выражалась через неё. После ряда работ Гёделя стрелку забыли в пользу коробки, в том числе потому, что в классическом варианте эти модальности взаимовыразимы. Как водится, в конструктивной формулировке симметрия распадается на независимые сущности, имеющие разные семантики - добавляя к строгим импликациям дополнительные схемы, можно получить логику для стрелок или любимой тотальщиками guarded recursion (кстати, как по русски - охраняемая рекурсия?).
https://arxiv.org/abs/1710.10805 Hou, Clouston, Gore, Tiu, "Modular Labelled Sequent Calculi for Abstract Separation Logics"
TIL откуда взялся фразеологизм "Господь, жги" - из пьесы "Огонь" омской группы "25/17": https://www.youtube.com/watch?v=5FpfQ3zqL1s (собственно сами слова звучат на 1:45)
YouTube
2Г5Р1О7Т(25:17) Огонь
https://www.ccs.neu.edu/home/turon/reagents.pdf Turon, "Reagents: Expressing and Composing Fine-grained Concurrency"
Underlying the shared state/message passing duality is a deeper one: Isolation versus Interaction. Operations on shared state are generally required to be atomic, which means in particular that they are isolated from one another; concurrent shared-state operations appear to be linearizable into a series of nonoverlapping, sequential operations. Synchronous message passing is just the opposite: rather than appearing to not overlap, sends and receives are required to overlap. Fine-grained concurrent operations straddle these two extremes, appearing to be isolated while internally tolerating (or exploiting) interaction.
Underlying the shared state/message passing duality is a deeper one: Isolation versus Interaction. Operations on shared state are generally required to be atomic, which means in particular that they are isolated from one another; concurrent shared-state operations appear to be linearizable into a series of nonoverlapping, sequential operations. Synchronous message passing is just the opposite: rather than appearing to not overlap, sends and receives are required to overlap. Fine-grained concurrent operations straddle these two extremes, appearing to be isolated while internally tolerating (or exploiting) interaction.
Хозяйке на заметку: диаграмма методов изготовления чая из https://en.wikipedia.org/wiki/Tea_processing.
Кстати, на днях начну мини-серию постов по формальным методам в ЖД, так что stay tuned!
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.108.573 Katis, Sabadini, Walters, [2002] "Feedback, trace and fixed-point semantics"
> a monoidal category in which the only arrows are identities is, ignoring the arrows, exactly a monoid structure on the objects, whereas a compact closed category with only identity arrows is an Abelian group. The notion of traced monoidal category in this special case turns out to be cancellative monoid.
> a monoidal category in which the only arrows are identities is, ignoring the arrows, exactly a monoid structure on the objects, whereas a compact closed category with only identity arrows is an Abelian group. The notion of traced monoidal category in this special case turns out to be cancellative monoid.
Евросоюз объявил 2021й годом железных дорог: https://europa.eu/year-of-rail/. При помощи разноцветных постеров еврократы ставят акценты на экологичности поездов и укреплении дружбы народов (она же "трансграничное сотрудничество"), но где-то на третьих-четвертых позициях мелькает и слово safety. Наиболее строгие гарантии безопасности даёт математика, что равносильно использованию формальных методов в инженерии, в частности формальной верификации. Используются ли такие вещи в железнодорожных целях, и если да, то как? Давайте начнём разбираться.
#railway
#railway
Что же можно и нужно верифицировать для поездов?
Современные железные дороги относят к так называемым киберфизическим системам. Это довольно новый термин, вошедший в оборот в нулевых. Он призван обозначать некоторую систему, имеющую как классические механические компоненты, описываемые “непрерывной” математикой и физикой, так и “дискретную” программную составляющую. Обычно здесь в пример приводят автономные автомобили, но под это описание подходят и устройства попроще, навроде конвеерной ленты на кассе магазина. Верифицируют в такого рода системах в первую очередь “дискретную” часть - т.е., софт и отдельно модели физических компонент, но существуют и гибридные подходы, до которых мы тоже дойдем.
Ключевая тема в железнодорожной безопасности это системы railway signalling (по русски СЦБ). Их разделяют на:
* interlocking, т.е. системы управления семафорами и стрелками, назначение которых - исключать конфликтующие маршруты. Как правило, сосредоточены вокруг станций.
* системы безопасности automatic train protection / control (по русски автоблокировки), в основном следящие за скоростью и дистанцией между составами. Действуют на всем протяжении линии.
* высокоуровневые системы automatic train operation (“автоведение”) и automatic train supervision, частично или полностью берущие на себя функции соответственно машиниста и диспетчера.
Важное направление работ - взаимная интеграция этих систем. Так, крупнейшим паневропейским железнодорожным проектом считается ERTMS, который понемногу вводят в ЕС с конца 90х. Он включает в себя СЦБ-подсистему ETCS, цель которой - стандартизировать работу национальных ATP и завершить переход на радио-протоколы. Аналогичным стандартом для метро и электричек является CBTC, внедряемый европейцами по всему миру с середины 80х. Так мы переходим к теме стандартов.
#railway
Современные железные дороги относят к так называемым киберфизическим системам. Это довольно новый термин, вошедший в оборот в нулевых. Он призван обозначать некоторую систему, имеющую как классические механические компоненты, описываемые “непрерывной” математикой и физикой, так и “дискретную” программную составляющую. Обычно здесь в пример приводят автономные автомобили, но под это описание подходят и устройства попроще, навроде конвеерной ленты на кассе магазина. Верифицируют в такого рода системах в первую очередь “дискретную” часть - т.е., софт и отдельно модели физических компонент, но существуют и гибридные подходы, до которых мы тоже дойдем.
Ключевая тема в железнодорожной безопасности это системы railway signalling (по русски СЦБ). Их разделяют на:
* interlocking, т.е. системы управления семафорами и стрелками, назначение которых - исключать конфликтующие маршруты. Как правило, сосредоточены вокруг станций.
* системы безопасности automatic train protection / control (по русски автоблокировки), в основном следящие за скоростью и дистанцией между составами. Действуют на всем протяжении линии.
* высокоуровневые системы automatic train operation (“автоведение”) и automatic train supervision, частично или полностью берущие на себя функции соответственно машиниста и диспетчера.
Важное направление работ - взаимная интеграция этих систем. Так, крупнейшим паневропейским железнодорожным проектом считается ERTMS, который понемногу вводят в ЕС с конца 90х. Он включает в себя СЦБ-подсистему ETCS, цель которой - стандартизировать работу национальных ATP и завершить переход на радио-протоколы. Аналогичным стандартом для метро и электричек является CBTC, внедряемый европейцами по всему миру с середины 80х. Так мы переходим к теме стандартов.
#railway
Wikipedia
Cyber–physical system
engineered systems built and operated with seamless integration between physical components and computation
Пока идёт работа над следующим постом, внес свой скромный вклад в дело победы логики 2.0 - небольшой стикер пак из иллюстраций "дизайнов" людики за авторством Жана-Ива Жирара.
https://www.tg-me.com/addstickers/Desseins
https://www.tg-me.com/addstickers/Desseins
В любом проекте по формальной верификации крайне важна спецификация - ведь корректность доказывают не “вообще” (что невозможно), а именно относительно строго заданной спецификации, как правило, закодированной формулами или “высказываниями” некоторой логики (в случае correct-by-construction программирования их роль играют типы некоторой достаточно мощной системы). Откуда же черпать спецификации для железных дорог?
В западном мире существуют два общепринятых семейства железнодорожных стандартов:
* евросоюзный CENELEC, от фр. Comité Européen de Normalisation ÉLECtrotechnique - на самом деле, как следует из названия, это целый комитет, публикующий сотни и тысячи регламентов на всевозможное электрооборудование; в контексте верификации ЖД нас интересуют стандарты EN50128 и EN50657, где EN это European Norm.
* североамериканский “набор рекомендаций” от AREMA (от American Railway Engineering and Maintenance-of-way Association), плюс военный стандарт для системного ПО MIL-STD-882.
Стандарты 50128 и 50657 регламентируют непосредственно создание и использование ПО для сигнальных систем и подвижных составов соответственно, они входят в более широкое семейство ЖД-стандартов, в частности 50126 (общий стандарт безопасности), 50129/50159 (сигнальные системы), 50155 (подвижные составы) и т.д. Распространяются они на все уровни ПО, потенциально влияющего на безопасность движения - от аппаратных прошивок и ядер ОС до пользовательских интерфейсов.
50128 существует в 2х вариантах: 2001 и 2011, которые совместимы в одну сторону (т.е, 2011 более строгий). Он вводит понятие Safety Integrity Level или SIL - это пронумерованные от 0 до 4 степени требуемой надежности программы. Использование формальных методов “рекомендуется” для уровней 1-2, и “крайне рекомендуется” для 3-4. Разработку предписывается вести по V-образной модели (см. диаграмму ниже).
В отношении формальных методов стандарт рекомендует: использовать их только для критических компонент, строить высокоуровневые иерархические модели, максимально дискретизируя переменные, и делать упор на автоматические доказательства. В качестве примеров ФМ приводятся:
* алгебры процессов CSP и CCS
* интерактивный пруф-ассистент HOL
* языки спецификаций LOTOS, OBJ, "темпоральная логика", VDM, Z-нотация
* B-метод
#railway
В западном мире существуют два общепринятых семейства железнодорожных стандартов:
* евросоюзный CENELEC, от фр. Comité Européen de Normalisation ÉLECtrotechnique - на самом деле, как следует из названия, это целый комитет, публикующий сотни и тысячи регламентов на всевозможное электрооборудование; в контексте верификации ЖД нас интересуют стандарты EN50128 и EN50657, где EN это European Norm.
* североамериканский “набор рекомендаций” от AREMA (от American Railway Engineering and Maintenance-of-way Association), плюс военный стандарт для системного ПО MIL-STD-882.
Стандарты 50128 и 50657 регламентируют непосредственно создание и использование ПО для сигнальных систем и подвижных составов соответственно, они входят в более широкое семейство ЖД-стандартов, в частности 50126 (общий стандарт безопасности), 50129/50159 (сигнальные системы), 50155 (подвижные составы) и т.д. Распространяются они на все уровни ПО, потенциально влияющего на безопасность движения - от аппаратных прошивок и ядер ОС до пользовательских интерфейсов.
50128 существует в 2х вариантах: 2001 и 2011, которые совместимы в одну сторону (т.е, 2011 более строгий). Он вводит понятие Safety Integrity Level или SIL - это пронумерованные от 0 до 4 степени требуемой надежности программы. Использование формальных методов “рекомендуется” для уровней 1-2, и “крайне рекомендуется” для 3-4. Разработку предписывается вести по V-образной модели (см. диаграмму ниже).
В отношении формальных методов стандарт рекомендует: использовать их только для критических компонент, строить высокоуровневые иерархические модели, максимально дискретизируя переменные, и делать упор на автоматические доказательства. В качестве примеров ФМ приводятся:
* алгебры процессов CSP и CCS
* интерактивный пруф-ассистент HOL
* языки спецификаций LOTOS, OBJ, "темпоральная логика", VDM, Z-нотация
* B-метод
#railway
Интересно, станет ли модным reversible computing в свете надвигающейся "циркулярной экономики"?