arXiv 0706.25442007-06-18cs.LO

抽象机器对话游戏

Abstract machines for dialogue games

Pierre-Louis Curien, Hugo Herbelin

摘要：

抽象的Boehm树的概念已经出现，作为一个面向操作的蒸馏工作的游戏语义，并已在两篇论文中进行了研究。本文重新审视了这个概念，提供了更多的语法支持和更多的例子（如按值调用评估），说明了底层计算设备的通用性。建立了抽象Boehm树评价机制的各种公式之间的精确对应关系。

英文摘要：

The notion of abstract Boehm tree has arisen as an operationally-oriented distillation of works on game semantics, and has been investigated in two papers. This paper revisits the notion, providing more syntactic support and more examples (like call-by-value evaluation) illustrating the generality of the underlying computing device. Precise correspondences between various formulations of the evaluation mechanism of abstract Boehm trees are established.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

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

继续探索

相关论文

角色的完全抽象游戏语义

Fully Abstract Game Semantics for Actors

基于参与者的代数理论和异步$π$演算的博弈语义，给出了参与者博弈语义的完全抽象证明。

2019-01-07cs.LO

Lorenzen对话游戏的结构理论

Toward a structure theory for Lorenzen dialogue games

洛伦岑对话提供了一种两人博弈的形式，可以描述各种逻辑：这种博弈的每一组规则$S$确定了一组公式$\mathcal{D}(S)$，其中一个玩家（所谓的Proponent）有一个获胜的策略，而这组$\mathcal{D}(S)$可以与各种逻辑相一致，例如直觉逻辑、经典逻辑、模态逻辑、连接逻辑和相关逻辑。但是，这些游戏所采用的标准规则集在逻辑上往往是不透明的，并且可能涉及彼此之间的微妙互动。此外，$\mathcal{D}(S)$可能以意想不到的方式与$S$发生变化; $S$中的小变化，即使是逻辑上动机良好的变化，也可能使$\mathcal{D}(S)$在逻辑上不寻常。我们提出的问题，提供一个结构理论，可以解释如何$\mathcal{D}(S)$与$S$变化，特别是，当$\mathcal{D}(S)$是封闭下的肯定前件（从而构成至少一个最小的逻辑）。

2013-12-16cs.LOmath.LO

游戏语义的抽象机器，再访

Abstract machines for game semantics, revisited

我们定义了新的抽象机器的游戏语义，对应于传统的计算机网络，并可以作为一个中间表示编译目标的分布式系统。这是通过两个步骤实现的。首先，我们介绍了HRAM，一个堆和寄存器抽象机，一个传统的计算机的抽象，它可以被构造成HRAM网，一个抽象的点对点网络模型。HRAM是多线程的，并且通过令牌进行子线程通信（参见或跳跃。游戏抽象机（GAM）是在接口级别具有额外结构的HRAM，但没有特殊的操作能力。我们表明，GAM不能天真地组成，但组成必须使用适当的HRAM组合子介导。HRAM足够灵活，可以表示具有状态（非无辜游戏）或并发（非交替游戏）的语言的游戏模型。我们说明了这种技术的潜力，通过实现一个玩具分布式编译器ICA，高阶程序设计语言与共享状态并发，从而显着扩展我们以前的分布式PCF编译器。我们表明，编译是健全的和内存安全的，即没有（分布式或本地）垃圾回收是必要的。

2013-04-15cs.LO

pi的全抽象并发对策

Fully-abstract concurrent games for pi

我们定义了一个语义米尔纳的π演算，有三个主要的新奇。首先，它提供了一个完全抽象的公平测试等价模型，而以前的语义涵盖了双相似性和可能和必须测试等价的变体。其次，它是基于约简语义，而以前的语义是基于标记的转换系统。最后，它具有Hyland-Ong和Nickau意义上的游戏语义色彩。事实上，我们的模型可以被视为一个无辜的预层语义和并发游戏语义。

2013-10-16cs.LO

战略论证是NP完全的

Strategic Argumentation is NP-Complete

NICTA（澳大利亚国家信息与通信技术机构）

在本文中，我们研究的复杂性战略论证的对话游戏。对话游戏是一个2人游戏，双方进行争论。我们展示了如何在一个怀疑的，非单调的形式主义的对话游戏模型，我们表明，决定什么移动（一套规则）在每一个回合玩的问题是一个NP完全问题。

2013-12-16cs.AIcs.CCcs.LO

一种基于动作语言的形式化抽象论证框架

An action language-based formalisation of an abstract argumentation framework

Sorbonne Université（索邦大学）；CNRS（法国国家科学研究中心）；ISIR（智能系统与机器人研究所）

本文提出一种纳入论证陈述顺序的抽象论证图建模新框架，可推导每个对话的唯一扩展，并证明终止性、正确性及两种完备性，其中通过“最后陈述最后更新”策略验证第二种完备性。

2024-09-29cs.AIcs.LO

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

不动点方程组的抽象、可达技术与对策

Abstraction, Up-to Techniques and Games for Systems of Fixpoint Equations

系统的不动点方程在完整的格，组成（混合）最小和最大的不动点方程，允许一个表达一些验证任务，如模型检查各种规格的逻辑或检查共归纳行为等价。在本文中，我们开发了一个理论的近似系统的不动点方程的抽象解释的风格：一个系统在一些具体的域被抽象到一个系统在一个合适的抽象域，与条件，确保抽象的解决方案代表一个声音/完全overapproximation的具体解决方案。有趣的是，最多技术，一个经典的方法，用于共归纳设置，以获得更容易或可行的证明，可以被解释为抽象的方式，他们自然适合我们的框架，并扩展到方程组。此外，依赖于近似理论，我们可以提供一个表征的解决方案的系统的不动点方程在一个合适的奇偶游戏方面的完整的格，概括了一些最近的工作，仅限于连续格。游戏的观点开辟了道路上的飞行算法的发展特点的解决方案，这样的方程系统。

2021-06-18cs.LO

谈判游戏（含摘要）

Negotiation Games (with abstract)

协商是一种以多方协商为原语的并发模型，最近在arXiv：1307.2145，arXiv：1403.4958中引入。我们开始研究这个模型的游戏。我们研究联盟的问题：可以一个给定的联盟的代理人的力量，谈判终止（分别。阻止谈判，使谈判永远进行下去）？联合部队能否确定谈判的结果？我们证明了任意协商的问题是EXPTIME完全的。然后，我们表明，声音和确定性，甚至弱确定性谈判的问题可以解决PTIME。请注意，问题的输入是一个协商，它可以比其状态空间呈指数级更紧凑。

2015-07-29cs.LO

名义通用引用的完全抽象

Full abstraction for nominal general references

游戏语义学已经在制定具有高阶过程和广泛的计算效果的语言的完全抽象语义方面取得了相当大的成功。最近，名义游戏已经提出了建模功能语言的名称。这些都是普通的，有状态的游戏投在理论的名义集开发的皮茨和Gabbay。在这里，我们采取名义游戏更进一步，通过开发一个完全抽象的语义语言与名义的一般参考。

2009-09-11cs.LOcs.PL

战略博弈中的函数依赖（扩展摘要）

Functional Dependence in Strategic Games (extended abstract)

本文研究了多人策略对策纳什均衡中局中人策略间函数依赖的性质。主要关注的是在支付函数的固定依赖图的上下文中函数依赖的属性。提出了一个描述任意给定图的函数依赖性质的逻辑系统，并证明了该系统是完备的。

2013-03-04cs.GTcs.LO

如何既富有又快乐：结合多人游戏的定量和定性战略推理

How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games (Extended Abstract)

我们提出了一个逻辑框架，结合了对多人博弈中代理人通过优化收益或结果偏好来实现定量目标的能力的博弈论研究，以及对玩家实现玩家定性目标的能力的逻辑分析，即，达到或保持具有期望属性的游戏状态。我们丰富的并发游戏模型与支付的范式游戏与模型的状态，并提出了一个定量扩展的逻辑ATL*，使定量和定性推理相结合。

2013-03-04cs.LOcs.MA

推理主义博弈语义（扩展摘要）

Inferentialist Game Semantics (Extended Abstract)

University College London（伦敦大学学院）；Institute of Philosophy, University of London（伦敦大学哲学研究所）

该研究探讨推理主义博弈语义，利用类似技术建立基扩展语义（B - eS）与海兰德 - 翁博弈语义的完全抽象关联，并通过4x4数独示例说明语义，为逻辑系统提供了基于证明计算的内涵意义理论。

2026-07-23cs.LOmath.LO

将博弈论扩展形式规范为抽象的5元关系

Specifying a Game-Theoretic Extensive Form as an Abstract 5-ary Relation

本文提出用满足八个公理的5元关系（pentaform）来规范博弈论扩展形式，并构造了pentaform博弈与传统博弈之间的直观双射，同时探讨了其在子博弈和完美回忆等方向的应用。

2024-09-30cs.GTcs.LOecon.TH

简单的游戏语义和Day卷积

Simple game semantics and Day convolution

游戏语义为各种程序设计语言提供了足够的模型，在这些语言中，类型被解释为两个玩家的游戏，程序被解释为策略。Melliès（2018）认为，这种博弈和策略的范畴可以作为弱双范畴上的简单抽象构造的实例来获得。然而，在简单游戏的特殊情况下，他的结构与标准类别略有不同。我们完善的抽象结构使用因式分解系统，并表明，新的建设产生的标准类别的简单的游戏和策略。另一个可能令人惊讶的例子是日的卷积monoidal结构的类别preheaves超过一个严格的monoidal类别。

2018-10-16cs.LOcs.PLmath.CT