<div dir="ltr">Hi,<div><br></div><div>I'm modelling pi calculus in Agda and having difficulty using sized types in order to have the function ⊖ below pass the termination-checker. <span style="color:rgb(0,0,0);font-family:Arial,'Liberation Sans','DejaVu Sans',sans-serif;font-size:14px;line-height:17.804800033569336px">I'm also getting an error message which looks a bit odd, so perhaps there's a clue to what I'm doing wrong in there.</span></div>
<div><font color="#000000" face="Arial, Liberation Sans, DejaVu Sans, sans-serif"><span style="line-height:17.804800033569336px"><br></span></font></div><div><div>{-# OPTIONS --sized-types #-}<br></div><div><div><br></div>
<div>module Temp where</div><div><br></div><div> open import Data.Product public hiding (swap)</div><div> open import Relation.Binary.PropositionalEquality</div><div> open import Size</div><div><br></div><div> -- Processes.</div>
<div> data Proc : Set where</div><div> ν_ : Proc → Proc</div><div><br></div><div> -- Actions.</div><div> data ⟿ᵇ : Set where</div><div> input : ⟿ᵇ</div><div> boundOut : ⟿ᵇ</div><div><br></div><div> data ⟿ᶜ : Set where</div>
<div> out : ⟿ᶜ</div><div><br></div><div> data ⟿ : Set where</div><div> _ᵇ : ⟿ᵇ → ⟿</div><div> _ᶜ : ⟿ᶜ → ⟿</div><div><br></div><div> -- Renamings. Leave undefined for now.</div><div> data Ren : Set where</div>
<div><br></div><div> postulate</div><div> push : Ren</div><div> swap : Ren</div><div> _ᴬ*_ : Ren → ⟿ᶜ → ⟿ᶜ</div><div><br></div><div> -- Transitions.</div><div> data _—[_]→_ : {ι : Size} → Proc → (a : ⟿) → Proc → Set where</div>
<div> ν•_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P (out ᶜ) R →</div><div> _—[_]→_ {ι = ↑ ι} (ν P) (boundOut ᵇ) R</div><div> νᵇ_ : ∀ {ι P R} {a : ⟿ᵇ} → _—[_]→_ {ι = ι} P (boundOut ᵇ) R →</div><div> _—[_]→_ {ι = ↑ ι} (ν P) (a ᵇ) (ν R)</div>
<div> νᶜ_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P ((push ᴬ* out) ᶜ) R →</div><div> _—[_]→_ {ι = ↑ ι} (ν P) (out ᶜ) (ν R)</div><div><br></div><div> infixl 0 _—[_]→_</div><div><br></div><div> postulate</div><div>
_ᴾ*_ : Ren → Proc → Proc</div><div> _ᵀ*_ : ∀ {ι} (ρ : Ren) {P R} {a : ⟿ᶜ} → _—[_]→_ {ι = ι} P (a ᶜ) R →</div><div> _—[_]→_ {ι = ι} (ρ ᴾ* P) ((ρ ᴬ* a) ᶜ) (ρ ᴾ* R)</div><div> swap-involutive : ∀ (P : Proc) → swap ᴾ* swap ᴾ* P ≡ P</div>
<div> swap∘push : swap ᴬ* push ᴬ* out ≡ out</div><div><br></div><div> infixr 8 _ᵀ*_ _ᴾ*_ _ᴬ*_</div><div><br></div><div> -- Structural congruence.</div><div> infix 4 _≅_</div><div> data _≅_ : Proc → Proc → Set where</div>
<div> νν-swap : ∀ P → ν (ν (swap ᴾ* P)) ≅ ν (ν P)</div></div><div><br></div><div><div> -- "Residual" of a transition E after a structural congruence φ.</div><div> ⊖ : ∀ {ι P P′} {a : ⟿} {R} (E : _—[_]→_ {ι = ι} P a R) (φ : P ≅ P′) →</div>
<div> Σ[ R ∈ Proc ] _—[_]→_ {ι = ι} P′ a R</div><div> ⊖ (ν•_ (νᶜ E)) (νν-swap P) with swap ᵀ* E</div><div> ... | swap*E rewrite swap-involutive P | swap∘push =</div><div> _ , {!!} -- νᵇ (ν• swap*E)</div><div>
⊖ E φ = {!!}</div></div><div><br></div><div>(I can try to boil the code down further if that would help, but I wanted to maintain some of the structure of my setting.)</div></div><div><br></div><div><div>In the first goal above, I'm matching on the situation where there are adjacent ν binders, and showing that if I transpose the binders (by applying the 'swap' renaming under the binders) then the associated steps in the derivation also tranpose. Intuitively this preserves the size of the transition derivation. And indeed, toggling hidden arguments reveals that the goal has type _—[_]→_ {↑ (↑ .ι)}, so I expect to be able to apply two constructors (νᵇ and ν• in this case) in return for two I eliminated (ν• and νᶜ). </div>
<div><br></div><div>I can also see that E has type _—[_]→_ {.ι}. Since I've postulated that ᵀ* is size-preserving, the variable swap*E also has this type. Naively, I expect νᵇ (ν• swap*E) to therefore be size-consistent with the goal. However Agda complains that the constraints are inconsistent.</div>
<div><br></div><div>Weirdly, if I use a "with" clause to introduce ν• swap*E into the context, I get the following error:</div><div><br></div><div>.ι !=< P of type Size</div><div>when checking that the expression E has type</div>
<div>swap ᴾ* P —[ (push ᴬ* out) ᶜ ]→ .R</div><div><br></div><div>This is baffling because the appearance of meta-variable P in the error message suggests that Agda is trying to match a size index against a variable of type Proc, does it not?</div>
<div><br></div><div>Can anyone shed any light on what's going on here?</div></div><div><br></div><div>many thanks,</div><div>Roly</div><div><br></div><div><br></div><div>Roly Perera</div><div>LFCS, School of Informatics</div>
<div>University of Edinburgh</div><div><br></div></div>