<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);">
Thank you so much for your reply!</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);">
1 ) Conal - Thanks for suggestion! It's nice to hear from you, especially given the fact I loved your paper on backpropagation I found some while a go!</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);">
2) Mietek - Thanks a lot! Just joined this channel and would love to discuss the problem I have. I do understand that my mail could have been cumbersome - sorry!</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);">
3) Wouter - The paper I am formalising is <a href="https://www.cs.tufts.edu/comp/150FP/archive/remi-douence/functional-vms.pdf" id="LPlnk403274">https://www.cs.tufts.edu/comp/150FP/archive/remi-douence/functional-vms.pdf</a> - Right now I have formalised the
first intermediate language and trying to formalise tranform Va (page 9, the paper has proof of it's well-typedness on page 46). Besides intrinsically typed version (my code: <a href="https://gist.github.com/wkr1u18/e32b670ce50b4ee248f7c72e80123b29" id="LPlnk176799">https://gist.github.com/wkr1u18/e32b670ce50b4ee248f7c72e80123b29</a>)
- I tried extrinsically typed version following the PLFA formalism ( here is what I have so far <a href="https://gist.github.com/wkr1u18/97ce47d221fc30b1f40c7e26b69eecd9" id="LPlnk812830">https://gist.github.com/wkr1u18/97ce47d221fc30b1f40c7e26b69eecd9</a>),
so I could separately define the transform on the terms and then prove the welltypedness of the transform.</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 style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Swierstra, W.S. (Wouter) <W.S.Swierstra@uu.nl><br>
<b>Sent:</b> 06 November 2020 07:30<br>
<b>To:</b> rozowski w.k. (wkr1u18) <wkr1u18@soton.ac.uk>; agda@lists.chalmers.se <agda@lists.chalmers.se><br>
<b>Subject:</b> Re: Converting intrinsically typed terms</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">CAUTION: This e-mail originated outside the University of Southampton.<br>
<br>
Hi Wojciech,<br>
<br>
Thanks for your message on the Agda mailing list. Which paper are you trying to formalize? That would really help me understand whether or not you're on the right track here.<br>
<br>
Good luck with your project!<br>
<br>
Wouter<br>
<br>
________________________________________<br>
From: Agda <agda-bounces@lists.chalmers.se> on behalf of rozowski w.k. (wkr1u18) <wkr1u18@soton.ac.uk><br>
Sent: Monday, 2 November 2020 11:55<br>
To: Agda users<br>
Subject: [Agda] Converting intrinsically typed terms<br>
<br>
Hello everyone!<br>
<br>
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.<br>
I am writing to ask for any advice how to formalise type correct transformations between intrinsically typed terms.<br>
<br>
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.<br>
<br>
The type rules (and way of building terms - because intrinsic typing) for those combinators, are:<br>
pushₛ_ : ∀ {Γ A}<br>
→ Γ ⊢ A<br>
-----<br>
→ Γ ⊢ Rₛ A<br>
<br>
ƛₛ_ : ∀ {Γ A B}<br>
→ Γ , A ⊢ B<br>
---------<br>
→ Γ ⊢ A ⇒ₛ B<br>
<br>
_∘_ : ∀ {Γ A B}<br>
→ Γ ⊢ Rₛ A<br>
→ Γ ⊢ A ⇒ₛ B<br>
---------<br>
→ Γ ⊢ B<br>
<br>
(Rs A is just annotated type for something of type A being stored on stack)<br>
<br>
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:<br>
<br>
ξ-∘ₛ₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ₛ B} {M : Γ ⊢ Rₛ A}<br>
→ L —→ L′<br>
---------------<br>
→ M ∘ L —→ M ∘ L′<br>
<br>
ξ-∘ₛ₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ₛ B} {M M′ : Γ ⊢ Rₛ A}<br>
→ Value V<br>
→ M —→ M′<br>
---------------<br>
→ M ∘ V —→ M′ ∘ V<br>
<br>
β-∘ₛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}<br>
-------------------<br>
→ (pushₛ W) ∘ (ƛₛ N) —→ N [ W ]<br>
<br>
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:<br>
<br>
Va : Λ→Λs<br>
<br>
Va [[x]] = pushs x<br>
Va [[λx.E]] = pushs (λsx.Va [[E]] )<br>
Va [[E1 E2]] = Va [[E2]] o Va [[E1]] o app with app = λsf.f<br>
<br>
As the STLC is the subset of the first combinator language, I just defined transform from the language to itself: I defined map between types, contexts and variables lookup<br>
<br>
Va-type : Type → Type<br>
Va-type (x ⇒ x₁) = Rₛ ( (Va-type x) ⇒ₛ (Va-type x₁) )<br>
Va-type `ℕ = Rₛ `ℕ<br>
Va-type (Rₛ x) = Rₛ (Va-type x)<br>
Va-type (x ⇒ₛ x₁) = (Va-type x) ⇒ₛ (Va-type x₁)<br>
<br>
Va-context : Context → Context<br>
Va-context ∅ = ∅<br>
Va-context (x , x₁) = ( Va-context x , Va-type x₁ )<br>
<br>
Va-var : ∀ {Γ A} → Γ ∋ A → ((Va-context Γ) ∋ (Va-type A))<br>
Va-var Z = Z<br>
Va-var (S x) = S Va-var x<br>
<br>
And the problematic part is declaring the transform between terms:<br>
<br>
Va : ∀ {Γ A} → Γ ⊢ A → (Va-context Γ) ⊢ (Va-type A)<br>
Va (` x) = ` Va-var x<br>
Va (ƛ x) = pushₛ (ƛₛ Va x)<br>
<br>
-- Here is the hole I cannot come up with filling it<br>
Va {Γ} (x · x₁) = (pushₛ (Va x₁)) ∘ ((pushₛ (Va x)) ∘ (ƛₛ {!!} ))<br>
Va `zero = pushₛ `zero<br>
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<br>
<br>
-- Combinators from intermediate language are mapped to itself<br>
Va (pushₛ x) = pushₛ Va x<br>
Va (ƛₛ x) = ƛₛ Va x<br>
Va (x ∘ x₁) = Va x ∘ Va x₁<br>
<br>
The only bit, I am not able to formalise is the "app" combinator, as standard lookup using #_ doesnt work when mapping between terms.<br>
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?<br>
<br>
I would be most grateful if I could hear back from you!<br>
<br>
Best,<br>
Wojciech<br>
</div>
</span></font></div>
</body>
</html>