A Weak Calculus With Explicit Operators For Pattern Matching And Substitution
RTA '02: Proceedings of the 13th International Conference on Rewriting Techniques and Applications（2002）
摘要
In this paper we propose a Weak Lambda Calculus called lambdaP(w) having explicit operators for Pattern Matching and Substitution. This formalism is able to specify functions defined by cases via pattern matching constructors as done by most modem functional programming languages such as OCAML. We show the main property enjoyed by lambdaP(w), namely subject reduction, confluence and strong normalization.
更多查看译文
关键词
Pattern Match, Free Variable, Reduction Rule, Typing Rule, Strong Normalization
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要