Інформатика

Мотивація

Важливим етапом в розвитку викладача є не тільки програма для вищої школи четвертого рівня акредитації, але і для середньої школи, а значить кожного учня в кожному селі. Для цих потреб за основу я хочу взяти програму "Інформатика" Манфреда Броя.

Власне, оскільки школа починається з 5 років приблизно, то цей курс у вигляді монографії повинен відповідати вимогам ELI5, шоб кожен вчитель міг відтворити цей курс.

Структура курсу Манфреда Броя

Шо гарного я можу сказати про цю програму: 1) це фулстек програма, яка покриває розробку мовних засобів, дискретну математику і паралельне програмування 2) програма викладається штучно створеною педагогічною мовою для цього типу паскаля 3) логіку починає з Арістотеля.

Чотири теми мого курсу Інформатика наслідують розділ на чотири книги Манфреда Броя і мають наступну структуру:

1) Основи: інформація, алгоритми і структури, мови, їх класи:
    — Інформація, інформаційна система та її властивості.
    — Позиційні системи числення, кодування інформації.
    — Алгоритми, системи переписування термів, ג-числення, рекурсія.
    — Типи і структури даних, Бом дерева, структурна рекурсія.
    — Логіка висловлювань, логіка предикатів, вищі логіки.
    — Мови програмування, граматики, БНФ, лексичний аналіз.
2) Дискретна математика, схемотехніка, асемблери:
    — Булева алгебра та редукція термів. ДНФ, КНФ;
    — Регістри, Лічильники, Логіка, Арифметика;
    — Архітектура компʼютера. SMP, AMP;
    — Узгоджена паралельна обробка черг.
3) Операційні системи, компілятори, рантайми;
    — Числення процесів. Моделі процесів. Мережі Петрі, FSM, BPMN.
    — Операційні системи і рантайми. Реактори, Процеси, Канали, Курсори.
    — Мови. Лексика, Синтаксис. LL, LR, LALR. Інтерпретатори, Компілятори.
4) Формальні мови, обчислювальність, складність, ефективність:
    — Формальні мови. Основи математики;
    — Обчислювальність. Коректність. Складність. Ефективність;
    — Семантика мов програмування. Формальні моделі;
    — Мова опису математики.

Інформація, алгоритми і структури даних, мови, типи, рекурсія. Інформатика. Інформація. Кодування. Логіка. Алгебра Буля. Інтерпретація. Властивості. Нормальні форми. Канонічність. Послідовності. Алгоритм. Терм реврайтінг. Детермінізм. Функції. Структури. Натруальні числа. Множини. Типи даних. Предикати. Мови програмування. БНФ. Аплікативні мови. Функціональні мови. Рекурсія. Мови доведення. Теореми. Повнота. Консистентність. Коректність.

Дискретна математика і схемотехніка.

Операційні системи, рантайми, інтерпретатори і компілятори.

Формальні мови, обчислювальність, коректність, слкадність, ефективність.

Компілятор мови ML Робіна Мілнера

Оскільки четверта тема є добре пропрацьованою в курсі "Формальна математика", а операційна система з третьої теми теж частина цієї монографії, то найскладніша і націкавіша теми, з якої хочеться почати --- це "Компілятор", який є частиною третьої теми курсу.

Я провів в дослідженні компіляторів, мов програмування і операційних систем 20 років, починаючи від embedded систем TRON, QNX, BeOS до дизасемблювання NT в Soft-ICE і хочу сказати шо ті школи які взяли у якості основи серію мов Standard ML мають неабияку перевагу. Я провів свою юність з мовами серії ML лише поверхово (написали веб-сокет сервер, портували на SML N2O та NITRO), але вже тоді схопив найголовніше: мова ML це єдина промислова мова рівня System F з доведеною семантикою і теоремами про коректність (soundness) написаними в Twelf, головна заслуга тут Роберта Харпера. Мова програмування Standard ML була придумана Робіном Мілнером за яку він дістав премію Тюрінга, один з небагатьох хто заслужено.

Тому замість Pascal/Ada-подібної мови Манфреда Броя, на якій наводяться приклади алгоритмів з його курсу "Інформатика" в нашому курсі ми пропонуємо використовувати ML мову MinCaml розроблену Ейдзіро Суміі в Університеті Токіо.