<div dir="ltr"><span style="color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px">Hi Wojciech. Since you are starting with the STLC, you might find it helpful to factor compilation through cartesian closed categories (CCCs). Then you can use a standard translation for the first part (STLC→CCCs) and define the rest as familiar algebraic operations: identity, sequential composition, projections, parallel composition, etc, all with standard laws they must satisfy (associativity of composition etc). I’ve described such an approach </span><a href="http://conal.net/papers/calculating-compilers-categorically/" style="color:rgb(153,153,204);font-family:sans-serif;font-size:17.8px">in a paper draft</a><span style="color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px">, and there’s a corresponding </span><a href="https://github.com/conal/calculating-compilers-agda" style="color:rgb(153,153,204);font-family:sans-serif;font-size:17.8px">Agda implementation</a><span style="color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px">. Best of luck! - Conal</span><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Nov 2, 2020 at 2:56 AM rozowski w.k. (wkr1u18) <<a href="mailto:wkr1u18@soton.ac.uk">wkr1u18@soton.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div dir="ltr">
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Hello everyone!</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
I'm relatively new to Agda (recently just went through first two Parts of PLFA), so I'm sorry if my question is obvious or don't appropriate for this forum.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
I am writing to ask for any advice how to formalise type correct transformations between intrinsically typed terms.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Currently, while doing my BSc thesis, I am working on formalizing a paper about framework for specifying abstract machines, as a series of transforms between STLC and intermediate languages including combinators (eg. pushₛ to push on stack, ƛₛ to pop from stack
and bind to variable, _∘_ to perform sequencing). Each intermediate language adds a pair of push and lambda combinators to work with different parts of machine - eg. environments, continuations. Each of the intermediate languages is a subset of the following
ones.</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
The type rules (and way of building terms - because intrinsic typing) for those combinators, are:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
pushₛ_ : ∀ {Γ A}
<div> → Γ ⊢ A</div>
<div> -----</div>
<div> → Γ ⊢ Rₛ A</div>
<div><br>
</div>
<div> ƛₛ_ : ∀ {Γ A B}</div>
<div> → Γ , A ⊢ B</div>
<div> ---------</div>
<div> → Γ ⊢ A ⇒ₛ B</div>
<div><br>
</div>
<div> _∘_ : ∀ {Γ A B}</div>
<div> → Γ ⊢ Rₛ A</div>
<div> → Γ ⊢ A ⇒ₛ B </div>
<div> ---------</div>
→ Γ ⊢ B</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
(R<sub>s </sub>A<sub> </sub>is just annotated type for something of type A being stored on stack)</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
I managed to use the PLFA formalism and add typing rules for lambda calculus extended with pair of combinators for the stack and sequencing operators. The extended semantics now include:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
ξ-∘ₛ₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ₛ B} {M : Γ ⊢ Rₛ A}
<div> → L —→ L′</div>
<div> ---------------</div>
→ M ∘ L —→ M ∘ L′<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
ξ-∘ₛ₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ₛ B} {M M′ : Γ ⊢ Rₛ A}
<div> → Value V</div>
<div> → M —→ M′</div>
<div> ---------------</div>
→ M ∘ V —→ M′ ∘ V<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
β-∘ₛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
<div> -------------------</div>
→ (pushₛ W) ∘ (ƛₛ N) —→ N [ W ]<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
The part I am having trouble with is formalising a transform between terms from STLC to this intermediate language. One of the transforms introduced by this paper is:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Va : Λ→Λ<sub>s</sub> </div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Va [[x]] = push<sub>s</sub> x </div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Va [[λx.E]] = push<sub>s</sub> (λ<sub>s</sub>x.Va [[E]] ) </div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Va [[E1 E2]] = Va [[E2]] o Va [[E1]] o app with app = λsf.f<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span style="color:rgb(0,0,0);font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt"> As the STLC is the subset of the</span><span style="color:rgb(0,0,0);font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt"> first combinator
language, I just defined transform from the language to itself: I defined map between types, contexts and variables lookup</span><br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span style="color:rgb(0,0,0);font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt"><br>
</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span style="color:rgb(0,0,0);font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt">Va-type : Type → Type
<div>Va-type (x ⇒ x₁) = Rₛ ( (Va-type x) ⇒ₛ (Va-type x₁) )</div>
<div>Va-type `ℕ = Rₛ `ℕ</div>
<div>Va-type (Rₛ x) = Rₛ (Va-type x)</div>
<div>Va-type (x ⇒ₛ x₁) = (Va-type x) ⇒ₛ (Va-type x₁)</div>
<div><br>
</div>
<div>Va-context : Context → Context</div>
<div>Va-context ∅ = ∅</div>
<div>Va-context (x , x₁) = ( Va-context x , Va-type x₁ )</div>
<div><br>
</div>
<div>Va-var : ∀ {Γ A} → Γ ∋ A → ((Va-context Γ) ∋ (Va-type A))</div>
<div>Va-var Z = Z</div>
Va-var (S x) = S Va-var x<br>
</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span style="color:rgb(0,0,0);font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt"><br>
</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span style="color:rgb(0,0,0);font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt">And the problematic part is declaring the transform between terms:</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Va : ∀ {Γ A} → Γ ⊢ A → (Va-context Γ) ⊢ (Va-type A)
<div>Va (` x) = ` Va-var x</div>
<div>Va (ƛ x) = pushₛ (ƛₛ Va x)</div>
<div><br>
</div>
<div>-- Here is the hole I cannot come up with filling it</div>
<div>Va {Γ} (x · x₁) = (pushₛ (Va x₁)) ∘ ((pushₛ (Va x)) ∘ (ƛₛ {!!} ))</div>
<div>Va `zero = pushₛ `zero</div>
<div>Va (`suc x) = pushₛ (`zero) -- paper doesn't provide any notion for dealing with sucessors of Nats - currently left like this to pass the typecheck</div>
<div><br>
</div>
<div>-- Combinators from intermediate language are mapped to itself</div>
<div>Va (pushₛ x) = pushₛ Va x</div>
<div>Va (ƛₛ x) = ƛₛ Va x</div>
Va (x ∘ x₁) = Va x ∘ Va x₁ <br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
The only bit, I am not able to formalise is the "app" combinator, as standard lookup using #_ doesnt work when mapping between terms. </div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Do you happen to have any advice for me, how to tackle such transformations? Is there anything I am missing in my way of formalising? Did any of you worked with type correct transformations of terms in de Brujin typed terms and have any tips for me?</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
I would be most grateful if I could hear back from you!</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Best,</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Wojciech</div>
</div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>