- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我想在 pi 演算的转移关系的推导上定义一个大小保持函数。我无法让 Agda 相信它确实可以保持大小。我还收到了一条看起来毫无意义的错误消息,所以也许其中有线索。
我尽可能地简化了代码,同时仍然保留了设置的风格。这是序言。
{-# OPTIONS --sized-types #-}
module SizedTypes where
open import Data.Product public hiding (swap)
open import Relation.Binary.PropositionalEquality
open import Size
-- Processes.
data Proc : Set where
ν_ : Proc → Proc
-- Actions.
data ⟿ᵇ : Set where
input : ⟿ᵇ
boundOut : ⟿ᵇ
data ⟿ᶜ : Set where
out : ⟿ᶜ
data ⟿ : Set where
_ᵇ : ⟿ᵇ → ⟿
_ᶜ : ⟿ᶜ → ⟿
-- Renamings.
data Ren : Set where
postulate
push : Ren
swap : Ren
_ᴬ*_ : Ren → ⟿ᶜ → ⟿ᶜ
-- Transitions.
data _—[_]→_ : {ι : Size} → Proc → (a : ⟿) → Proc → Set where
ν•_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P (out ᶜ) R →
_—[_]→_ {ι = ↑ ι} (ν P) (boundOut ᵇ) R
νᵇ_ : ∀ {ι P R} {a : ⟿ᵇ} → _—[_]→_ {ι = ι} P (boundOut ᵇ) R →
_—[_]→_ {ι = ↑ ι} (ν P) (a ᵇ) (ν R)
νᶜ_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P ((push ᴬ* out) ᶜ) R →
_—[_]→_ {ι = ↑ ι} (ν P) (out ᶜ) (ν R)
infixl 0 _—[_]→_
postulate
_ᴾ*_ : Ren → Proc → Proc
_ᵀ*_ : ∀ {ι} (ρ : Ren) {P R} {a : ⟿ᶜ} → _—[_]→_ {ι = ι} P (a ᶜ) R →
_—[_]→_ {ι = ι} (ρ ᴾ* P) ((ρ ᴬ* a) ᶜ) (ρ ᴾ* R)
swap-involutive : ∀ (P : Proc) → swap ᴾ* swap ᴾ* P ≡ P
swap∘push : swap ᴬ* push ᴬ* out ≡ out
infixr 8 _ᵀ*_ _ᴾ*_ _ᴬ*_
-- Structural congruence.
infix 4 _≅_
data _≅_ : Proc → Proc → Set where
νν-swap : ∀ P → ν (ν (swap ᴾ* P)) ≅ ν (ν P)
现在这是我做不到的。
-- "Residual" of a transition E after a structural congruence φ.
⊖ : ∀ {ι P P′} {a : ⟿} {R} (E : _—[_]→_ {ι = ι} P a R) (φ : P ≅ P′) →
Σ[ R ∈ Proc ] _—[_]→_ {ι = ι} P′ a R
⊖ (ν•_ (νᶜ E)) (νν-swap P) with swap ᵀ* E
... | swap*E rewrite swap-involutive P | swap∘push =
_ , {!!} -- νᵇ (ν• swap*E)
⊖ E φ = {!!}
粗略地说,我在匹配有相邻 ν 个 Binder 的情况,并表明如果我转置 Binder (通过在 Binder 下应用“交换”重命名),那么推导中的相关步骤也会转置。直观上,这保留了转换推导的大小。
切换隐藏参数(在 Emacs 中)显示有问题的子句中的目标具有类型 _—[_]→_ {↑ (↑ .ι)}
,所以我希望能够应用两个构造函数(在本例中为 νᵇ 和 ν•)。我还可以看到 E 的类型为 _—[_]→_ {.ι}
,swap*E
也是,所以我(天真地)期望 νᵇ (ν• swap*E)
与目标大小一致。然而 Agda 提示约束不一致。
奇怪的是,如果我使用 with
子句将 ν• swap*E
引入上下文,则会出现以下错误:
.ι !=< P of type Size
when checking that the expression E has type
swap ᴾ* P —[ (push ᴬ* out) ᶜ ]→ .R
这令人费解,因为元变量 P 的选择表明 Agda 正在尝试将大小索引与 Proc 类型的变量相匹配。
我在这里做错了什么?
最佳答案
感谢 Andrea Vezzosi 在 Agda 邮件列表上回答这个问题。在这种情况下,它就像显式传递 ι 索引一样简单:
⊖ (ν• (νᶜ_ {ι} E)) (νν-swap P) with swap ᵀ* E
... | swap*E rewrite swap-involutive P | swap∘push
= _ , νᵇ (ν•_ {ι = ι} swap*E)
关于termination - 无法解决的尺寸限制,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/25307334/
@Cacheable在同一类中方法调用无效 上述图片中,同一个类中genLiveBullets()方法调用同类中的queryLiveByRoom()方法,这样即便标识了Cacheable标签,
目录 @Transaction注解导致动态切换更改数据库失效 使用场景 遇到问题 解决 @Transaction
@RequestBody不能class类型匹配 在首次第一次尝试使用@RequestBody注解 开始加载字符串使用post提交(貌似只能post),加Json数据格式传输的时候,
目录 @Autowired注入static接口问题 @Autowired自动注入普通service很方便 但是如果注入static修饰的serv
目录 @RequestBody部分属性丢失 问题描述 JavaBean实现 Controller实现
目录 解决@PathVariable参数接收不完整的问题 今天遇到的问题是: 解决办法: @PathVariable接受的参
这几天在项目里面发现我使用@Transactional注解事务之后,抛了异常居然不回滚。后来终于找到了原因。 如果你也出现了这种情况,可以从下面开始排查。 1、特性 先来了解一下@Trans
概述: ? 1
场景: 在处理定时任务时,由于这几个方法都是静态方法,在aop的切面中使用@Around注解,进行监控方法调用是否有异常。 发现aop没有生效。 代码如下:
最近做项目的时候 用户提出要上传大图片 一张图片有可能十几兆 本来用的第三方的上传控件 有限制图片上传大小的设置 以前设置的是2M&nb
我已经实现了这个SCIM reference code在我们的应用程序中。 我实现的代码确实通过了此postman link中存在的所有用户测试集合。 。我的 SCIM Api 也被 Azure 接受
我一直对“然后”不被等待的行为感到困扰,我明白其原因。然而,我仍然需要绕过它。这是我的用例。 doWork(family) { return doWork1(family)
我正在尝试查找 channel 中的消息是否仍然存在,但是,我不确定如何解决 promise ,查看其他答案和文档,我可以看到它可能是通过函数实现的,但我是不完全确定如何去做。我希望能在这方面获得一些
我有以下情况: 同一工作区中的 2 个 Eclipse 项目:Apa 和 Bepa(为简洁起见,使用化名)。 Apa 项目引用(包括)Bepa 项目。 我在 Bepa 有一个类 X,具有公共(publ
这个问题已经有答案了: Why am I getting a NoClassDefFoundError in Java? (31 个回答) 已关闭 6 年前。 我正在努力学习 spring。所以我输入
我正在写一个小游戏,屏幕上有许多圆圈在移动。 我在两个线程中管理圈子,如下所示: public void run() { int stepCount = 0; int dx;
我在使用 Sympy 求解方程时遇到问题。当我运行代码时,例如: 打印(校正(10)) 我希望它打印一个数字 f。相反,它给我错误:执行中止。 def correction(r): from
好吧,我制作的每个页面都有这个问题。我不确定我做错了什么,但我所有的页面都不适用于所有分辨率。可能是因为我使用的是宽屏?大声笑我不确定,但在小于宽屏分辨率的情况下,它永远不会看起来正确。它的某些部分你
我正在尝试像这样进行一个非常简单的文化 srting 检查 if(culture.ToUpper() == "ES-ES" || "IT-IT") { //do something } else
Closed. This question is off-topic. It is not currently accepting answers. Learn more。 想改进这个问题吗?Upda
我是一名优秀的程序员,十分优秀!