上下文无关语言上的函数的实用类型检查

摘要

本文介绍函数式语言LFC的一种类型检查方法。LFC语言是为支持软件形式规约的获取和检验工作而开发的一个通用的形式规约语言。该语言使用并结合了形式语言和递归函数这两种功能的强大的数学工具。由此，LFC语言在保持很强的表达能力的同时，也使得在规约获取过程中使用机器学习和其他机器辅助技术成为可能。LFC语言的理论基础是一种新的递归函数。