Николай Вячеславович Шилов

В математике неподвижной точкой функции $F\colon D\to D$ называется решение уравнения $F(x)=x$. Например, если $F\colon\mathbb R\to\mathbb R$ — функция $x^2+x-1$, то неподвижная точка этой функции — любое решение уравнения $x^2+x-1=x$; очевидно, что это уравнение имеет два решения $x_1=-1$ и $x_2=1$ и, следовательно, $-1$ и $1$ являются неподвижными точками этой функции.

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

• теорема Банаха (1922) о неподвижной точке широко используется в вычислительной математике;
• теоремы Брауэра (~1910) и Какутани (1941) о неподвижной точке широко известна благодаря её применению в теории стратегических игр (и связи с понятием равновесия Нэша в частности).

Однако наш курс будет посвящен другой теореме – теореме Кнастера-Тарского о неподвижной точке монотонной функции (операции) на полных решётках. Она была доказана Брониславом Кнастером (1928) и обобщёна Альфредом Тарским (1955).

На первом занятии мы познакомимся с конечными позиционными играми, выигрышными стратегиями и представлением множества позиций с выигрышной стратегией в виде неподвижной точки монотонной функции на множестве всех подмножеств позиций игры.

На втором занятии мы познакомимся с понятием полной решетки, сформулируем теорему Кнастера-Тарского о неподвижных точках монотонной операции на полных решётках и докажем её для случая конечных решёток. Далее мы применим полученную теорию к решению простой головоломки об игре в числа и наметим алгоритм для более сложной головоломки.

Третье занятие будет посвящено использованию теоремы Кнастера-Тарского в спецификации программных систем средствами так называемой Computation Tree Logic (CTL).

Четвёртое занятие будет посвящено использованию теоремы Кнастера-Тарского для автоматической верификации CTL-спецификаций методом проверки моделей (model checking). За разработку этого метода верификации Эдмунд М. Кларк, Аллен Эмерсон и Иосиф Сифакис в 2007 г. были удостоены премии им. Алана Тьюринга.

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