首页/论文/1608.03535

arXiv 1608.035352016-08cs.PLcs.DB

SQL的直觉逻辑程序设计

Intuitionistic Logic Programming for SQL (Extended Abstract)

Fernando Sáenz-Pérez

备注：: Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

直觉主义逻辑编程提供了规则体中嵌入式蕴涵的概念，它可以用来推理由前件修改的当前数据库。这可以应用于将SQL转换为Datasheet以解决SQL WITH查询的系统，对于这些查询，关系是本地定义的，因此可以理解为添加到当前数据库。此外，SQL查询中的假设（如添加或删除数据）也可以用这种方式建模，这对于决策支持场景来说是一个有趣的特性。这项工作提出了一种将直觉逻辑编程应用于SQL的方法，并提供了一个实现这一思想的工作系统的指针。

英文摘要：

Intuitionistic logic programming provides the notion of embedded implication in rule bodies, which can be used to reason about a current database modified by the antecedent. This can be applied to a system that translates SQL to Datalog to solve SQL WITH queries, for which relations are locally defined and can therefore be understood as added to the current database. In addition, assumptions in SQL queries as either adding or removing data can be modelled in this way as well, which is an interesting feature for decision-support scenarios. This work suggests a way to apply intuitionistic logic programming to SQL, and provides a pointer to a working system implementing this idea.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

从计算演示合成解析SQL矩阵

Synthesizing Analytical SQL Queries from Computation Demonstration

分析型SQL广泛应用于现代数据库应用程序和数据分析。然而，它的划分和分组操作符对于新手用户来说是具有挑战性的。不幸的是，在标准SQL上显示有效的示例编程不太吸引人，因为分析查询的示例手工解决起来更费力。为了使演示更容易创建，我们设计了一个新的最终用户规范，通过计算演示编程，允许用户使用（可能不完整的）单元级计算跟踪来演示任务。该规范被利用在一个新的基于抽象的合成算法，以证明一个部分形成的查询不能完成，以满足规范，允许我们修剪的搜索空间。我们在名为Sickle的工具中实现了我们的方法，并在80个真实分析SQL任务上对其进行了测试。结果表明，即使是小规模的演示，Sickle也可以在平均12.8秒内解决76个任务，而之前的方法只能解决60个任务，平均速度要慢22.5倍。我们对13名参与者的用户研究表明，我们的规范提高了用户在挑战性任务上的效率和信心。

2022-04-22cs.DBcs.PL

逻辑框架下的高阶抽象推理

Reasoning with Higher-Order Abstract Syntax in a Logical Framework

基于具有更高类型量化的直觉或线性逻辑的逻辑框架已成功地用于对程序设计语言和推理系统领域中的许多重要判断给出高级、模块化和形式化的规范。给定这样的规范，考虑证明框架中指定系统的属性是很自然的：例如，给定函数式程序设计语言的求值规范，证明该语言是确定性的或求值保留类型。开发这种推理框架的一个挑战是高阶抽象语法（HOAS），一种优雅的和声明性的对象级抽象和替换处理，很难在涉及归纳的证明中处理。在本文中，我们提出了一个元逻辑，可用于推理使用HOAS编码的判断，这个元逻辑是一个简单的直觉主义逻辑，承认高阶量化简单类型的非线性项（HOAS的关键成分），以及归纳和定义的概念的扩展。我们通过考虑直觉和线性逻辑的编码，探讨了HOAS编码的形式元理论分析的困难，并正式推导出这些逻辑的重要子集的割的容许性。然后，我们提出了一种方法，以避免高阶抽象语法的好处和分析所产生的编码的能力之间的明显的权衡。我们通过涉及简单函数式和命令式程序设计语言PCF和PCF：=的示例来说明这种方法。我们正式推导出这样的属性，作为唯一性的类型，主题减少，确定性的评价，和等价的过渡语义和自然语义表示的评价。

2001-01-15cs.LOcs.PL

约束逻辑程序设计在SQL语义分析中的应用

Applying Constraint Logic Programming to SQL Semantic Analysis

Complutense University of Madrid（马德里康普顿斯大学）

本文提出了使用约束逻辑编程（CLP）的SQL查询建模在一个数据独立的抽象层，专注于一些语义属性，在这样的查询信号可能的错误。首先，我们定义一个从SQL到Datasheet的转换，以及从Datasheet到CLP的转换，这样解决这个CLP程序将给出关于不一致性、重言式和可能的简化的信息。我们使用不同的约束域映射到SQL类型，并建议他们合作，以提高准确性。我们的方法利用演绎系统，包括SQL和数据库，我们提出了一个实现在这个系统中，目前正在课堂上进行测试，显示其优势和差异相对于其他方法，以及一些性能数据。本文件正在考虑被TPLP接受。

2019-07-25cs.AIcs.DBcs.LO

一种查询语言中间表示的设计

Design of an intermediate representation for query languages

面向数据的应用程序通常是用高级通用程序设计语言（如Java）编写的，通过粗糙的接口与数据库进行交互。非正式地说，查询的文本在应用程序端构建（通过普通的字符串连接或通过语句的抽象概念），并通过线路发送到执行它的数据库。然后将结果序列化并发送回“客户端代码”，在那里它们被翻译成语言的本地数据库。这种往返对性能是有害的，但更糟糕的是，这样的编程模型阻止了人们具有更丰富的查询，即包含用户定义函数（即由程序员定义并例如在SQL查询的过滤条件中使用的函数）的查询。虽然一些数据库也拥有“服务器端”语言（例如Oracle数据库中的PL/SQL），但它与非常优化的查询执行引擎的集成仍然很小，并且包含（PL/SQL）用户定义函数的查询仍然非常低效。在这种情况下，我们回顾了现有的语言集成查询框架，强调现有的数据库查询语言（包括SQL）共享高级查询原语（例如，过滤、连接、聚合），它们可以由运算符表示，但是在它们的表达语言的语义方面有很大的不同。为了以与应用程序语言和数据库无关的方式表示查询，我们设计了一个小演算，称为“QIR”的查询中间表示。QIR包含对应于纯λ演算的小扩展的表达式，以及表示常见查询基元的运算符。为了向数据库发送有效的查询，我们在QIR术语的测量中抽象出了“好”查询表示的想法。然后，我们设计了一个评估策略重写QIR查询表示为“更好”的。

2016-07-14cs.PL

指称语义实验

An experiment with denotational semantics

本文介绍了如何按“逆序”，即从表示到语法，系统地设计一门程序设计语言。这种结构是在一个代数框架中开发的，该框架由三个多排序代数组成：表示法，抽象语法和具体语法。这些代数是以这样一种方式构造的，即从具体语法到指称存在唯一的同态，这构成了语言的指称语义。除了它的代数框架，该模型是集合论的，即指称域只是集合，而不是斯科特的自反域。该方法说明了一个虚拟语言Lingua的逐层开发：一个应用层，一个命令层（递归过程）和一个SQL层，其中Lingua被视为一个API（应用程序编程接口）的SQL引擎。后者也被赋予了指称语义。该语言配备了强大的打字机制，涵盖了基本类型（数字，布尔等），列表、数组、记录及其任意组合，以及类似SQL的类型：行、表和数据库。类型模型包括SQL完整性约束。

2019-05-04cs.PL

数据布局的类型论视角

Data Layout from a Type-Theoretic Perspective

本文提出一种基于直觉主义逻辑半公理相继式演算的类型论数据布局方法，通过细化地址结构支持替代布局，并添加递归类型，可作为编译器中间语言或增强程序员控制。

2023-02-21cs.LOcs.PL

更多相关论文收起更多论文

逻辑程序设计的证明理论基础综述

A Survey of the Proof-Theoretic Foundations of Logic Programming

一些形式系统，如归结和最小模型语义，为逻辑编程提供了一个框架。在本文中，我们将调查使用结构证明理论作为替代基础。在过去的35年里，研究人员一直在使用这个基础来将逻辑编程从一阶经典逻辑的根源提升到直觉和线性逻辑的高阶版本。这些更具表现力的逻辑程序设计语言允许捕获有状态计算和丰富形式的抽象，包括高阶编程、模块化和抽象数据类型。术语级绑定是另一种抽象，在证明理论和这些扩展逻辑程序设计语言中，它们都得到了优雅而直接的处理。逻辑编程也激发了证明理论的新成果，例如涉及极性和聚焦证明的成果。这些最新的研究结果提供了一个高层次的手段，呈现前向链和后向链风格推理之间的差异。在证明论中验证逻辑编程也有助于识别它与函数式编程、演绎数据库和模型检验的联系和区别。

2021-10-30cs.LOcs.PL

类型化抽象类的扩展初始化

Extended Initiality for Typed Abstract Syntax

初始语义学的目标是将与签名相关联的语法解释为某类“模型”的初始对象，为抽象语法产生归纳和递归原则。Zavió证明了一个简单类型语法的初始性结果：给定一个签名S，与S相关联的抽象语法构成了单子中S的模型范畴中的初始对象。然而，她的定理提供的迭代原则只考虑了在一组固定的对象类型上的两种语言之间的翻译。我们推广Zavió的模型概念，使对象类型可以变化，产生一个更大的类别，同时保持其中语法的初始性。因此，我们得到了一个扩展的初始性定理的类型化抽象语法，在不同类型的条款之间的翻译可以指定通过相关的范畴理论的迭代算子作为一个初始态射。我们的定义确保通过初始化指定的翻译是类型安全的，即在明显的意义上与源语言和目标语言中的类型兼容。我们的主要例子是通过命题作为类型的范例：我们指定命题和推理规则的经典和直觉命题逻辑通过各自的类型签名。然后，我们使用范畴论的迭代算子指定一个双重否定翻译从前者到后者。第二个例子是PCF的签名。对于这种特殊情况，我们在证明助手Coq中将定理形式化。然后，我们指定，通过范畴理论的迭代运算符，从PCF的无类型的λ演算的翻译。

2012-04-05cs.LOcs.PL

利用大型语言模型自动发现数据库管理系统测试 oracle

Automated Discovery of Test Oracles for Database Management Systems Using LLMs

UC Berkeley（加州大学伯克利分校）；National University of Singapore（新加坡国立大学）；Tsinghua University（清华大学）

本文提出Argus框架，利用LLM生成语义等价的SQL骨架，并通过形式化证明确保正确性，从而自动发现数据库管理系统中的测试oracle，发现40个新bug。

2026-03-24cs.DBcs.PLcs.SE

丰富线性/非线性λ演算：一种用于字符串图的程序设计语言

Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams

线性/非线性（LNL）模型，如Benton所描述的，合理地建模了与直觉线性逻辑密切相关的LNL项演算和LNL逻辑。每一个这样的模型诱导一个典型的丰富，我们显示健全模型的LNL λ演算弦图，介绍了里奥斯和塞林格（主要应用于量子计算）。我们对这种语言的抽象处理导致了比迄今为止提出的更简单的具体模型。我们还扩展了一般递归的语言，并证明合理性。最后，我们提出了一个充分的结果，对应于修改后的版本的本顿和Wadler的伴随演算与递归的语言的无干扰片段。

2018-04-25cs.LOcs.PLmath.CT