Просмотр исходного текста страницы Рефал — опыт формализации в преподавании информатики (Даниил Исакевич, OSEDUCONF-2023)

;{{SpeakerInfo}}: {{Speaker|Даниил Исакевич}}
<blockquote>
Представлен опыт использования связки Рефала, вычислителя программ в структурном стиле 
и LaTeX в работе преподавателя информатики строительного колледжа. На примере задачи 
вычисления таблицы истинности выражения в логике высказываний подробно описаны: опыт 
автоматической массовой генерации примеров и ответов, вынуждающий преподавателя учиться, 
и устройство генератора. Показаны некоторые возможности, которые отказ от стандартной 
реализации арифметики может дать преподавателю. Отмечены преимущества написания 
Рефал-программ с русскими именами переменных и функций.
</blockquote>

{{VideoSection}}
{{vimeoembed|908078468|800|450}}
{{youtubelink|NuvYuxQW-B0}}
{{SlidesSection}}
[[File:Рефал — опыт формализации в преподавании информатики (Даниил Исакевич, OSEDUCONF-2023).pdf|left|page=-|300px]]

{{----}}

== Thesis ==
Цель настоящего доклада — представить годичный (2022 г.) опыт использования Рефала 
и свободного программного обеспечения внештатным преподавателем информатики (первый 
курс обучения, фактически повторяющий восьмой класс школы).

=== Автоматическая массовая генерация примеров и ответов ===

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

*  вынуждает самого преподавателя учиться в ходе формализации примеров;
*  обеспечивает максимально возможное разнообразие примеров в рамках заданного формализма.


Имеющиеся в виде бумажных распечаток у преподавателя и свободно раздаваемые студентам примеры 
(к которым у преподавателя имеются ответы) используются как материал для объяснения, 
а также как массив тестовых заданий.

Генерация выражений и таблиц истинности производится под управлением Bash-скрипта, запускающего 
последовательное выполнение следующих действий:


# Вычисляется массив достаточно больших (от 1 до 10!) псевдослучайных целых чисел <m>S_k</m>. Выбор вычислителя продиктован личными предпочтениями автора (<tt>GNU Octave</tt>, но мог бы быть и <tt>Scilab</tt>).
# Программа на Рефале строит последовательность структурных выражений Рефала, представляющих выражения логики высказываний, каждое из которых содержит заданное число переменных и	связок. Выражение строится как дерево, выбор разбиения дерева на поддеревья, а также переменных и связок (включая 2-, 3- и 4-местные варианты $\wedge$, <m>\vee</m>) зависит от <m>{S_k}\textrm{ mod }{N_k}</m>, где <m>N_k</m> — число вариантов k-ого выбора, делаемого программой.
# Программа на Рефале преобразует последовательность сгенерированных выражений в последовательность	команд <tt>GNU Octave</tt> для вычисления таблицы истинности, выводимую в <tt>M</tt>-файл.
#  <tt>GNU Octave</tt> выполняет созданный <tt>M</tt>-файл, выводя таблицы истинности.
#  Программа на Рефале преобразует последовательность сгенерированных выражений в размеченный для LaTeX документ примеров. Другая программа на Рефале преобразует вычисленные таблицы истинности в размеченный для LaTeX документ ответов.
#  Документы примеров и ответов выводятся pdflatex в PDF-файлы и открываются для просмотра.


Передача данных между программами осуществляется через файлы, содержащие текст и доступные 
для анализа по окончании генерации. Целостность данных на всех этапах (от автоматической 
генерации до свободного оборота бумажных распечаток) обеспечивается:

*  сквозной (по всем этапам обработки) нумерацией сгенерированных выражений и таблиц истинности, передаваемой в составе обрабатываемых данных;
*  указанием даты и времени вёрстки в нижнем колонтитуле каждого PDF-файла.


Связка Рефала для преобразования структурированных текстов, вычислителя программ в структурном стиле и LaTeX для вёрстки документов с формулами была использована автором для генерации примеров и ответов по другим темам; успех не был достигнут там, где отсутствовала приемлемая формализация (в частности, при работе с блок-схемами и «цифровыми схемами»).

=== Отказ от стандартной реализации арифметики ===

Второе направление, для продвижения в котором был применён Рефал, возникло при освоении тем 
«измерение количества информации» и «позиционные системы счисления». Выяснилось, что отказ 
от стандартной реализации арифметики и представление числа цепочкой символов текста позволяют 
в ряде случаев использовать Рефал как вычислитель «абсолютной точности». К таким случаям относятся:

*  перевод «из килобитов в гигабайты» — все действия сводятся к умножению и делению на степени 2; получающиеся числа и дроби могут быть очень длинными, но всегда конечные;
*  перевод конечной десятичной дроби в позиционную систему с другим основанием может дать периодическую бесконечную дробь, запись которой с использованием скобок тем не менее конечна.


«Абсолютно точные» вычисления позволяют выявлять ошибки, совершаемые студентами при счёте, 
в том числе использование калькуляторов. Отказ же от стандартной реализации арифметики позволяет 
ставить студентам нестандартные задачи, решений (и онлайн-калькуляторов для которых) нет в Интернете.

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

=== Использованный инструментарий ===

Использованы ALT Linux p9 Starterkit (Hypericum), GNU Octave и TeXLive из репозитория пакетов. Для Рефала использованы Refal-5 Version PZ ([http://www.botik.ru/pub/local/scp/refal5/]) и интерпретатор Рефал-М ([https://github.com/STrusov/refal-machine]).

На Рефал-М возможно писать программы, читаемые как связный текст с русскими словами и словосочетаниями. 
Пропадает необходимость помнить или реконструировать громоздкие отождествления русских понятий с 
англоязами (часто кривыми). Мысль можно выразить в программе по-разному, но с богатством выразительных 
возможностей русского языка альтернативы могут стать более явными.


{{----}}
[[File:{{#setmainimage:Рефал — опыт формализации в преподавании информатики (Даниил Исакевич, OSEDUCONF-2023)!.jpg}}|center|640px]]
{{LinksSection}}
<!-- <blockquote>[©]</blockquote> -->

<references/>

[[Категория:OSEDUCONF-2023]]
[[Категория:Draft]]
[[Категория:СПО в образовании]]