论文标题
实验功能编程中可检查的元逻辑的实用惯用注意事项
Practical Idiomatic Considerations for Checkable Meta-Logic in Experimental Functional Programming
论文作者
论文摘要
在强大的，纯粹的功能性语言中实现复杂的概念作为可执行模型，在单纯的模拟和形式规范之间达到了一个甜蜜的位置。对于研究和教育，通常需要使用元逻辑注释来丰富算法代码，并体现为断言，定理或测试案例。检查框架使用功能范式的固有逻辑能力来近似通过启发式测试证明定理。在这里，我们提出了几个新颖的成语，以增强检查的实践表达，即元语言标记，名义的公理和建设性存在。所有这些都是在识字haskell'98中配制的，并具有一些通用的语言扩展。将它们的使用和影响通过应用于现实的建模问题来说明。
Implementing a complex concept as an executable model in a strongly typed, purely functional language hits a sweet spot between mere simulation and formal specification. For research and education it is often desirable to enrich the algorithmic code with meta-logical annotations, variously embodied as assertions, theorems or test cases. Checking frameworks use the inherent logical power of the functional paradigm to approximate theorem proving by heuristic testing. Here we propose several novel idioms to enhance the practical expressivity of checking, namely meta-language marking, nominal axiomatics, and constructive existentials. All of these are formulated in literate Haskell'98 with some common language extensions. Their use and impact are illustrated by application to a realistic modeling problem.
