Generalized Partial Computation (GPC) is a program transformation method utilizing partial information about input data, properties of auxiliary functions and the logical structure of a source program. GPC uses both a...Generalized Partial Computation (GPC) is a program transformation method utilizing partial information about input data, properties of auxiliary functions and the logical structure of a source program. GPC uses both an inference engine such as a theorem prover and a classical partial evaluator to optimize programs. Therefore, GPC is more powerful than classical partial evaluators but harder to implement and control. We have implemented an experimental GPC system called WSDFU (Waseda Simplify Distribute Fold Unfold). This paper discusses the power of the program transformation system, its theorem prover and future works.展开更多
This paper presents a program development system based on rewriting techniques. An introduction to an earlier version of the system without the verification system can be found in [1]. This paper focuses on the verifi...This paper presents a program development system based on rewriting techniques. An introduction to an earlier version of the system without the verification system can be found in [1]. This paper focuses on the verification subsystem which is designed to prove the correctness of the optimization rules and test equations in programs and specifications, hence to further guarantee the soundness of the program development process. The main technique employed in the verification subsystem is rewriting induction featured with batch proof method and witnessed test sets.展开更多
针对函数式程序模板元编程的通用性问题,以应用类型系统ATS(Applied Type System)为例,提出了一种基于元建模的模板元编程实现方法。基于ATS模板元编程给出从枚举类型Datatype到Function的生成实例;通过元建模构造了包含Datatype与Funct...针对函数式程序模板元编程的通用性问题,以应用类型系统ATS(Applied Type System)为例,提出了一种基于元建模的模板元编程实现方法。基于ATS模板元编程给出从枚举类型Datatype到Function的生成实例;通过元建模构造了包含Datatype与Function定义的ATS元模型;详细描述了Datatype模型到Function模型的转换;最后以一个基于元建模的ATS模板元编程为例,讨论了该方法的使用效果。实验结果表明该方法可以提高ATS模板元编程的通用性。展开更多
文摘Generalized Partial Computation (GPC) is a program transformation method utilizing partial information about input data, properties of auxiliary functions and the logical structure of a source program. GPC uses both an inference engine such as a theorem prover and a classical partial evaluator to optimize programs. Therefore, GPC is more powerful than classical partial evaluators but harder to implement and control. We have implemented an experimental GPC system called WSDFU (Waseda Simplify Distribute Fold Unfold). This paper discusses the power of the program transformation system, its theorem prover and future works.
文摘This paper presents a program development system based on rewriting techniques. An introduction to an earlier version of the system without the verification system can be found in [1]. This paper focuses on the verification subsystem which is designed to prove the correctness of the optimization rules and test equations in programs and specifications, hence to further guarantee the soundness of the program development process. The main technique employed in the verification subsystem is rewriting induction featured with batch proof method and witnessed test sets.
文摘针对函数式程序模板元编程的通用性问题,以应用类型系统ATS(Applied Type System)为例,提出了一种基于元建模的模板元编程实现方法。基于ATS模板元编程给出从枚举类型Datatype到Function的生成实例;通过元建模构造了包含Datatype与Function定义的ATS元模型;详细描述了Datatype模型到Function模型的转换;最后以一个基于元建模的ATS模板元编程为例,讨论了该方法的使用效果。实验结果表明该方法可以提高ATS模板元编程的通用性。
