基于等价关系的扩张切触代数的表示定理

Representation theorems for extended contact algebras based on equivalence relations

Philippe Balbiani, Tatyana Ivanova

DOI：: 10.1007/s11225-020-09923-0

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

本文的目的是给出扩张切触代数的新的表示定理。这些表示定理是基于等价关系。

英文摘要：

The aim of this paper is to give new representation theorems for extended contact algebras. These representation theorems are based on equivalence relations.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

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

继续探索

相关论文

次sigma-代数偏序集的Domain理论研究（扩展摘要）

A domain-theoretic investigation of posets of sub-sigma-algebras (extended abstract)

给定一个可测空间（X，M），M的次sigma-代数与X上的等价关系之间存在（Galois）联系。另一方面，X上的等价关系与随机关系上的同余密切相关。在最近的工作中，Doberkat研究了随机关系上的同余偏序集的格属性，并激发了对这些有序集的域理论研究。在这里，我们表明，偏序集的子西格玛代数的可测空间不享有所需的域理论的性质，我们的反例可以应用到一组光滑的等价关系的解析空间，从而给出了一个相当不满意的答案Doberkat的问题。

2010-06-02cs.LOmath.LO

多形类型的米田归约（扩展版）

The Yoneda Reduction of Polymorphic Types (Extended Version)

在本文中，我们探讨了一个家庭的类型同构的系统F的有效性，语义对应的某种形式的Yoneda同构从范畴论。这些同构在比β-η-等价更强的等价理论下成立，就像那些由参数性和非自然性引起的理论一样。我们表明，米田型同构产生重写的类型，我们称之为米田减少，它可以用来消除量词从多态类型，取代它们与单态类型构造函数的组合。我们建立了一些充分条件下，量词可以完全消除多态类型，我们展示了一些应用这些条件来计算居民的类型和计算程序等价系统F的一些片段。

2020-10-30cs.LOmath.LO

简化认知逻辑程序的强等价性（扩展版）

Strong Equivalence for Epistemic Logic Programs Made Easy (Extended Version)

认知逻辑程序（ELP），即扩展了认知算子的应答集程序设计（ASP），近年来引起了人们的新的兴趣，引发了一系列新的研究，也带来了高效的求解器。一个重要的问题是，在什么条件下，一个子程序可以被另一个子程序取代，而不改变其含义。这个问题被称为强等价，并且在ASP。对于ELP，这个问题已经通过将它们嵌入到平衡逻辑的认知扩展中来解决。在本文中，我们考虑一个更简单，更直接的表征，是直接适用于国家的最先进的ELP求解器中使用的语言。这也使我们能够给出严格的复杂性界限，表明ELP的强等价性仍然是coNP完全的，就像ASP一样。我们进一步使用我们的结果提供重言式规则和ELP的规则包容的句法特征。

2018-11-12cs.CCcs.LO

近似概率语境下互模拟与迹等价的关系（扩展版）

On the Relationship between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context (Extended Version)

这项工作介绍了一个概念的近似概率迹等价标记马尔可夫链，并将这个新的概念，已知的概念近似概率互模拟。特别是这项工作表明，后者的概念诱导一个严格的上限之间的近似有限的地平线的痕迹，所表示的总变化距离。因此，这项工作扩展了相应的结果，确切的概念和类似的结果，非概率模型。这个界限可以被用来关联在有界线性时间属性上的满意概率的接近程度，并且允许通过抽象对具体模型进行概率模型检验。的贡献集中在有限状态和不可数状态标记的马尔可夫链，并要求两个主要的应用：首先，它允许的上界的迹距离被确定为有限状态系统;其次，它可以被用来合成离散近似连续状态模型与任意精度。

2017-04-27cs.LO

浮点单元与高级C模型的等价性检查（扩展版）

Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version)

半导体公司越来越多地采用一种从C/C++/SystemC的系统级设计规范开始的方法。该模型经过广泛模拟，以确保正确的功能和性能。随后，在Verilog中创建寄存器传输级（RTL）实现，可以由设计人员手动创建，也可以由高级综合工具自动创建。必须检查C和Verilog程序是否一致。在本文中，我们提出了一个两步的方法，体现在两个等价性检查工具，VERIFOX和HW-CBMC，分别在软件和RTL级验证设计。VERIFOX用于对C中的非定时软件模型与C中的高级参考模型进行等价性检查。HW-CBMC验证了一个Verilog RTL实现与一个C语言非定时软件模型的等价性。为了评估我们的工具，我们将它们应用于ARM的商业浮点运算单元（FPU）和开源双路浮点加法器。

2016-09-01cs.LOcs.SE

术语重写系统中直到重命名的句法等价判定的复杂性（扩展版）

Complexity of Deciding Syntactic Equivalence up to Renaming for Term Rewriting Systems (Extended Version)

从程序转换的问题的动机，八个概念之间的同构术语重写系统的定义，分析和分类。这些概念包括全局同构，其中变量和函数符号的重命名对于系统的所有项重写规则都是相同的，局部同构，其中每个规则使用单个重命名，以及组合，其中一个符号集被全局重命名，而另一个符号集被局部重命名。保存语义属性，如可转换性和终止分析不同的同构概念。引入了项重写系统的模板和极大范式的概念，并给出了有效计算它们的算法。配备这些技术，同构的基本决策问题的复杂性进行了分析，并被证明是有效的解决或证明是完整的图同构复杂性类。

2022-11-30cs.LO

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

概率按需调用的λ演算--扩展版

A Probabilistic Call-by-Need Lambda-Calculus -- Extended Version

为了支持声明性概率程序设计语言的理解，我们引入了一个公平的二进制概率λ演算，选择其参数之间的概率相等的微积分。演算的归约策略是一种按需调用的策略，它执行惰性求值并通过递归let表达式实现共享。表达式的期望收敛是所有成功约简输出之和的极限，并按其概率加权。我们使用上下文等价作为程序语义：两个表达式是上下文等价的，当且仅当插入任何程序上下文的表达式的预期收敛总是相同的。我们开发和说明的技术，证明等价，包括上下文引理，两个派生的标准，以显示等价和一个基于语法的方法。这最终使我们能够显示一个大的程序转换的上下文等价的正确性。

2022-05-30cs.LO