函数作为类型，或函数依赖的“霍尔逻辑”
计算机科学中的逻辑
2012-10-18 v1
摘要
受编程理论统一化趋势的启发，本文展示了标准数据依赖理论的代数处理如何为关系数据配备函数类型及相关的类型系统，该类型系统对于数据库操作的类型检查和查询优化非常有用。然后表明，这种类型化的数据库编程方法与其他编程逻辑（例如霍尔逻辑或用于分析while语句的最强不变函数逻辑）属于同一家族。本文还考虑了在此代数方法之上使用自动推理系统（如Prover9）进行类型检查和查询优化的前景。
引用
@article{arxiv.1210.4661,
title = {Functions as types or the "Hoare logic" of functional dependencies},
author = {Jose N. Oliveira},
journal= {arXiv preprint arXiv:1210.4661},
year = {2012}
}