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

20

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

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

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

Дэйв Кларк
источник
9
«Молодой человек, в математике вы ничего не понимаете. Вы просто привыкаете к ним ». - Джон фон Нейман. К сожалению, привыкание к нему занимает годы, по крайней мере, в моем случае :)
uli
1
Интересно, почему некоторые люди (не обязательно вы, Дейв) думают, что всеобъемлющее образование бакалавра / магистра по CS (около пяти лет) можно заменить парой курсовых кредитов.
Рафаэль
Под «Теорией Б» вы ссылаетесь на «Метод Б»? en.wikipedia.org/wiki/B-Method
Стивен Шоу,
@StevenShaw: Нет. Теория B охватывает семантику и так далее, в отличие от автоматов / сложности.
Дейв Кларк,
Я не слышал о «Теории Б» раньше. Мне удалось найти этот полезный ответ на cstheory. Cstheory.stackexchange.com/a/1523/9552
Стивен Шоу,

Ответы:

14

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

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

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

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

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

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

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

улы
источник
3
Я не прошу ярлык; скорее путь (который короток).
Дэйв Кларк,
@JD Вопрос ОП говорит, что «ограниченный опыт работы в математике и формальных аспектах информатики» и «разбираются в использовании формальных методов и чтении статей». Если ученик имеет ограниченное знакомство с формализмом, используемым в математике и т. Д., Не стоит работать над теоретической темой. Он должен работать над основами, прежде чем делать следующий шаг. Я просто указывал на начало пути.
Uli
9

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

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

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

источник
Хорошее предложение, хотя я волнуюсь, является ли эта монография немного более плотной для начала. Это конечно тяжело.
Дейв Кларк,
5

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

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

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

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

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

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

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

Удай Редди
источник
У меня был какой-то умный, насмешливый ответ на это, включающий исчисление Длительности и каламбур на имя Куайна ... но, к сожалению, я об этом забываю ...
Дэйв Кларк