Путь к формальным методам

Нередки случаи, когда студенты начинают свои кандидатские диссертации с ограниченным опытом в математике и формальных аспектах информатики. Очевидно, что таким студентам будет очень трудно стать теоретиками компьютерных наук, но было бы хорошо, если бы они научились использовать формальные методы и читать статьи, содержащие формальные методы.

Каков хороший краткосрочный путь, по которому начинающие аспиранты могли бы пойти, чтобы получить разоблачение, необходимое для того, чтобы заставить их читать документы, используя формальные методы, и в конечном итоге писать документы, использующие такие формальные методы?

С точки зрения контекста, я думаю больше с точки зрения Теории B и формальной проверки как видов вещей, которые они должны изучить, но также и классических тем TCS, таких как теория автоматов.

В предисловии к своей книге «Математическое открытие, понимание, изучение и решение задач обучения» Джордж Поля пишет:

Решение проблем - это практическое искусство, такое как плавание, катание на лыжах или игра на пианино: научиться этому можно только подражанием и практикой. Эта книга не может предложить вам волшебный ключ, который открывает все двери и решает все проблемы, но она предлагает вам хорошие примеры для подражания и много возможностей для практики: если вы хотите научиться плавать, вы должны пойти в воду, и если вы Если вы хотите решить проблемы, вы должны решать проблемы.

Я думаю, что нет короткого пути, особенно для достижения состояния написания документов. Это требует практики, многое из этого.

Некоторые указатели:

Если «ограниченный фон в математике и формальные аспекты» означает «никогда не задумывали доказательство и написали его вниз» , то что - то вроде этого может быть началом.

Если что-то на листе теоретической информатики заставит студента чувствовать себя неловко, то желательно пройти курс повышения квалификации в соответствующей области математики.

Есть много источников для математического письма: конспекты лекций по 1978 Стэнфордского университета CS209 , конечно , возможно. Или эта статья Пола Халмоса.

Формальные методы, такие как Z, B, TLA, CafeObj, в значительной степени полагаются на теорию множеств, логику, теорию категорий, лямбда-исчисление и автоматы для моделирования концепций типов, данных и вычислений.

Вы можете перейти к всеобъемлющей монографии, такой как « Логика спецификационных языков», под редакцией Dines Bjørner и Martin C. Henson, «Монографии в теоретической информатике», Springer Verlag, 2008, и учиться по мере необходимости и использовать ссылки, цитируемые там. Или изучите одну тему за раз:

1. Теория множеств
2. Математическая логика
3. Временная логика
4. Универсальная алгебра
5. Лямбда-исчисление
6. Теория категорий

Я действительно думаю, что «формальные» методы не очень хорошая идея для образовательных целей. В этом отношении программирование компьютера является «формальным» методом. Удастся ли это как образовательный инструмент?

Что нужно, так это понимание, интуиция и способность справляться с абстракцией. Формальные методы мешают всему этому. Скорее, они продвигают метод проб и ошибок, хакинг, сопоставление с образцом, имитацию, акцентируя внимание на синтаксисе. У этого списка нет конца.

Любая часть строгой математики научит людей правильно рассуждать. Чем проще домен, тем лучше. Все, что я узнал о рассуждениях, я узнал в старшей школе, когда серьезно занялся евклидовой геометрией. Исчисление и линейная алгебра в университете сделали все остальное.

Другой привлекательной альтернативой является философская логика, где они учат людей думать о высказываниях и понимать, что такое информационный контент и что является следствием чего. Они делают это, не утопая учеников в символах.

Если вы подведете итоги всех ведущих компьютерных ученых, вы будете удивлены тем, сколько из них имеют формальное обучение философии. Мы теряем все это сейчас, потому что студенты-философы теперь думают о компьютерных науках как о мирском предмете. Привлечение наших студентов к изучению философии может до некоторой степени противостоять этому. Заставьте их работать через Историю Западной философии Бертрана Рассела . Это будет творить чудеса.

Если они работают в теории языка программирования, вы также можете прочитать Куайна, которого я считаю «крестным отцом» денотационной семантики. (Куайн, по сути, занимался денотационной семантикой естественного языка в Word и Object , что послужило огромным источником вдохновения для Кристофера Стрейчи. Но эта книга довольно сложна.) Отредактированная коллекция Quintessence - хороший источник идей Куайна для начинающего.

[Примечание добавлено: Одно из преимуществ философии перед математикой заключается в том, что учащиеся видят дебаты , т. Е. Они видят «правильный» аргумент и «неправильный» аргумент и видят, как эксперты разрушают неправильные. В математике никто никогда не видит неправильный аргумент, который ограничивает его образовательную ценность.]