<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body 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>
</body>
</html>