Algebraic steppers help students learn functional programming by displaying evaluation as a sequence of small-step reductions, but even simple programs produce long traces in which key ideas are buried under mundane reductions. This paper presents the filtered stepper calculus, a formal framework that gives users scoped, pattern-based control over which reduction steps are shown or hidden. Users annotate programs with lightweight filter expressions that match on the structure of redexes. Filters compose via lexical scoping so that inner filters override outer ones. We prove preservation, progress, and a simulation theorem establishing that the filtered stepper agrees with the underlying unfiltered semantics, and mechanize all proofs in Agda. We implement the calculus in the Hazel live programming environment, including its support for stepping programs with holes and type errors. To do so, we reconcile Hazel's internal environment-based evaluator with the substitution-based presentation expected in the classroom. We deploy the system in a university programming languages course. Our evaluation shows that students adopt the stepper organically, though more advanced uses of filters may require further instruction, and that instructors can use filters to craft focused traces for use in lectures.


翻译:暂无翻译

0
下载
关闭预览

相关内容

Stabilizing Transformers for Reinforcement Learning
专知会员服务
61+阅读 · 2019年10月17日
Hierarchically Structured Meta-learning
CreateAMind
27+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
29+阅读 · 2019年5月18日
Unsupervised Learning via Meta-Learning
CreateAMind
44+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
18+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
半监督多任务学习:Semisupervised Multitask Learning
我爱读PAMI
18+阅读 · 2018年4月29日
Focal Loss for Dense Object Detection
统计学习与视觉计算组
12+阅读 · 2018年3月15日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
5+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
12+阅读 · 2008年12月31日
Arxiv
10+阅读 · 2021年2月26日
VIP会员
最新内容
分层反无人机系统发展新趋势
专知会员服务
5+阅读 · 9月3日
何为协作武器?
专知会员服务
9+阅读 · 9月1日
《理解认知战:超越信息》
专知会员服务
13+阅读 · 9月1日
美国战争部在GenAI.mil上推出OpenAI的ChatGPT Mil
专知会员服务
8+阅读 · 8月31日
人工智能赋能军事维护:重新定义国防战备
专知会员服务
5+阅读 · 8月31日
《美陆军野战手册(2026年):特种部队》
专知会员服务
8+阅读 · 8月31日
相关VIP内容
Stabilizing Transformers for Reinforcement Learning
专知会员服务
61+阅读 · 2019年10月17日
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
27+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
29+阅读 · 2019年5月18日
Unsupervised Learning via Meta-Learning
CreateAMind
44+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
18+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
半监督多任务学习:Semisupervised Multitask Learning
我爱读PAMI
18+阅读 · 2018年4月29日
Focal Loss for Dense Object Detection
统计学习与视觉计算组
12+阅读 · 2018年3月15日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
5+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
12+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员