Семинары
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Ближайшие семинары
Календарь семинаров
Список семинаров
Архив по годам
Регистрация семинара

Поиск
RSS
Ближайшие семинары






Общеинститутский семинар «Коллоквиум МИАН»
5 декабря 2013 г. 16:00, г. Москва, конференц-зал МИАН (ул. Губкина, 8)
 


Доказуемо рекурсивные функции

Л. Д. Беклемишев
Видеозаписи:
Flash Video 692.6 Mb
Flash Video 4,150.0 Mb
MP4 692.6 Mb

Количество просмотров:
Эта страница:1147
Видеофайлы:383
Youtube Video:

Л. Д. Беклемишев
Фотогалерея


Видео не загружается в Ваш браузер:
  1. Проверьте с Вашим администратором, что из Вашей сети разрешены исходящие соединения на порт 8080
  2. Сообщите администратору портала о данной ошибке



Аннотация: Вычислимая функция $f\colon N\to N$ называется доказуемо рекурсивной в данной формальной теории $T$, если существует алгоритм её вычисления такой, что в $T$ можно доказать утверждение «для любого $x$ существует $y$ такой, что $f(x)=y$». В математической логике такие функции изучаются по двум причинам. Во-первых, для данной программы нас часто интересует доказательство её корректности, в частности вопрос о том, завершает ли она работу при любых исходных данных. Разработка методов верификации программ — важный раздел Computer Science. С другой стороны, мы можем использовать доказуемо рекурсивные функции для изучения и сравнения между собой различных формальных теорий. Такой подход приводит к изучению функций, имеющих катастрофически большой рост и наиболее впечатляющим на сегодняшний день примерам недоказуемых комбинаторных утверждений.

ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru
 
Обратная связь:
 Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2022