论文标题
使用Haskell计划教简单的建设性证明
Teaching Simple Constructive Proofs with Haskell Programs
论文作者
论文摘要
近年来，我们在我们的大化大学课程中探索了Haskell与传统的数学形式主义以及包括逻辑和形式语言在内的主题的课程，旨在为我们的学生提供有关这些数学主题的编程观点。我们已经发现，几乎可以通过互动学习平台提供几乎所有形成性和总结性的评估，并将Haskell作为我们广泛的教学大纲中的数字练习的通用语言。转换为这种格式的最难练习之一是传统的书面证明传达了建设性的论点。在本文中，我们反思了这种练习的数字化。我们分享了许多旨在针对类似技能的Haskell练习的例子，以在命题逻辑和正式语言中跨主题进行书面证明练习，讨论此类练习设计的各个方面。我们还对这些练习的响应进行了分类。这项讨论有助于我们对编程问题作为一种灵活的学习和评估的灵活数字媒体的更广泛探索。
In recent years we have explored using Haskell alongside a traditional mathematical formalism in our large-enrolment university course on topics including logic and formal languages, aiming to offer our students a programming perspective on these mathematical topics. We have found it possible to offer almost all formative and summative assessment through an interactive learning platform, using Haskell as a lingua franca for digital exercises across our broad syllabus. One of the hardest exercises to convert into this format are traditional written proofs conveying constructive arguments. In this paper we reflect on the digitisation of this kind of exercise. We share many examples of Haskell exercises designed to target similar skills to written proof exercises across topics in propositional logic and formal languages, discussing various aspects of the design of such exercises. We also catalogue a sample of student responses to such exercises. This discussion contributes to our broader exploration of programming problems as a flexible digital medium for learning and assessment.
