범위 지정된 필터를 활용한 실용적인 대수적 스텝핑 (Practical Algebraic Stepping with Scoped Filters)

대수적 스텝퍼 (Algebraic steppers)는 평가 과정을 작은 단계의 축약 (small-step reductions) 시퀀스로 보여줌으로써 학생들이 함수형 프로그래밍 (functional programming)을 배우는 데 도움을 주지만, 심지어 간단한 프로그램조차도 핵심 아이디어가 평범한 축약 과정 아래 묻혀버리는 긴 추적 (traces)을 생성합니다. 본 논문은 사용자가 어떤 축약 단계 (reduction steps)를 보여주거나 숨길지에 대해 범위 지정된 패턴 기반 제어 (scoped, pattern-based control)를 제공하는 공식 프레임워크인 필터링된 스텝퍼 계산법 (filtered stepper calculus)을 제시합니다. 사용자는 리덱스 (redexes)의 구조와 일치하는 가벼운 필터 표현식 (filter expressions)을 사용하여 프로그램에 주석을 답니다. 필터는 어휘적 범위 지정 (lexical scoping)을 통해 합성되므로, 내부 필터가 외부 필터를 재정의합니다. 우리는 보존 (preservation), 진행 (progress), 그리고 필터링된 스텝퍼가 필터링되지 않은 기본 의미론 (unfiltered semantics)과 일치함을 입증하는 시뮬레이션 정리 (simulation theorem)를 증명하며, 모든 증명을 Agda에서 기계화합니다. 우리는 구멍 (holes)과 타입 오류 (type errors)가 있는 프로그램을 스텝핑하는 지원 기능을 포함하여, Hazel 라이브 프로그래밍 환경 (live programming environment)에 이 계산법을 구현합니다. 이를 위해 Hazel의 내부 환경 기반 평가기 (environment-based evaluator)와 강의실에서 기대되는 치환 기반 제시 방식 (substitution-based presentation)을 조화시킵니다. 우리는 이 시스템을 대학 프로그래밍 언어 강의에 배포합니다. 우리의 평가 결과에 따르면, 학생들은 스텝퍼를 유기적으로 채택하지만 필터의 더 고급 사용법은 추가적인 교육이 필요할 수 있으며, 강사들은 강의에서 사용할 집중된 추적 (focused traces)을 제작하기 위해 필터를 사용할 수 있음을 보여줍니다.