<div dir="ltr"><div dir="ltr">I'd love to hear more as well.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Nov 6, 2020 at 3:24 PM Aaron Stump <<a href="mailto:aaron-stump@uiowa.edu">aaron-stump@uiowa.edu</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"><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Nov 6, 2020 at 5:53 AM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.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 lang="EN-GB">
<div>
<p class="MsoNormal"><span>I don’t agree that one should use CCCs because CCCs introduce the misleading identification of contexts and types. It is preferable to use a contextual version of CCCs, basically Categories with
 Families for simple types. I can provide more details if there is interest.<u></u><u></u></span></p><span></span></div></div></blockquote><div><br></div><div><div dir="ltr">Yes, please!<br></div></div><div><br></div><div>Aaron <br></div><div><br></div><div><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 lang="EN-GB"><div><span> </span>
<p class="MsoNormal"><span>Thorsten<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div style="border-color:rgb(181,196,223) currentcolor currentcolor;border-style:solid none none;border-width:1pt medium medium;padding:3pt 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:12pt;color:black">From: </span></b><span style="font-size:12pt;color:black">Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Conal Elliott <<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>><br>
<b>Date: </b>Wednesday, 4 November 2020 at 16:52<br>
<b>To: </b>"rozowski w.k. (wkr1u18)" <<a href="mailto:wkr1u18@soton.ac.uk" target="_blank">wkr1u18@soton.ac.uk</a>><br>
<b>Cc: </b>Agda users <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject: </b>Re: [Agda] Converting intrinsically typed terms<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:13.5pt;font-family:Arial,sans-serif;color:black">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/" target="_blank"><span style="font-size:13.5pt;font-family:Arial,sans-serif;color:rgb(153,153,204)">in a paper draft</span></a><span style="font-size:13.5pt;font-family:Arial,sans-serif;color:black">,
 and there’s a corresponding </span><a href="https://github.com/conal/calculating-compilers-agda" target="_blank"><span style="font-size:13.5pt;font-family:Arial,sans-serif;color:rgb(153,153,204)">Agda implementation</span></a><span style="font-size:13.5pt;font-family:Arial,sans-serif;color:black">.
 Best of luck! - Conal</span><u></u><u></u></p>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal">On Mon, Nov 2, 2020 at 2:56 AM rozowski w.k. (wkr1u18) <<a href="mailto:wkr1u18@soton.ac.uk" target="_blank">wkr1u18@soton.ac.uk</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border-color:currentcolor currentcolor currentcolor rgb(204,204,204);border-style:none none none solid;border-width:medium medium medium 1pt;padding:0cm 0cm 0cm 6pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Hello everyone!<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">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.<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">I am writing to ask for any advice how to formalise type correct transformations between intrinsically typed terms.<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">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</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> to push on stack, ƛ</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 to pop from stack and bind to variable, _</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;color:black">_ 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.<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">The type rules (and way of building terms - because intrinsic typing) for those combinators, are:<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">  push</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">_ :
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∀</span><span style="font-size:12pt;color:black"> {Γ A}
<u></u><u></u></span></p>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → Γ </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> A<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">      -----<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → Γ </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> R</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 A<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">  ƛ</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">_  :
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∀</span><span style="font-size:12pt;color:black"> {Γ A B}<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → Γ , A </span>
<span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> B<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">      ---------<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → Γ </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> A
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⇒</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> B<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">  _</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;color:black">_ :
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∀</span><span style="font-size:12pt;color:black"> {Γ A B}<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → Γ </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> R</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 A<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → Γ </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> A
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⇒</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> B
<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">      ---------<u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → Γ </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> B<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">(R_sAis just annotated type for something of type A being stored on stack)<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">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:<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">  ξ-</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">₁
 : </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∀</span><span style="font-size:12pt;color:black"> {Γ A B} {L L′ : Γ
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> A
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⇒</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> B} {M : Γ
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> R</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 A} <u></u><u></u></span></p>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → L —→ L′<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">      ---------------<u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → M </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;color:black"> L —→ M
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;color:black"> L′<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">  ξ-</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">₂
 : </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∀</span><span style="font-size:12pt;color:black"> {Γ A B} {V : Γ
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> A
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⇒</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> B} {M M′ : Γ
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> R</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 A} <u></u><u></u></span></p>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → Value V<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → M —→ M′<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">      ---------------<u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    → M </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;color:black"> V —→ M′
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;color:black"> V<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">  β-</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 :  </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∀</span><span style="font-size:12pt;color:black"> {Γ A B} {N : Γ , A
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> B} {W : Γ
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> A}
<u></u><u></u></span></p>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">      -------------------<u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">    →  (push</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> W)
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;color:black"> (ƛ</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 N) —→ N [ W ]<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">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:<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va : Λ→Λ_s <u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va [[x]] = push_s x <u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va [[λx.E]] = push_s (λ_sx.Va [[E]] ) <u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va [[E1 E2]] = Va [[E2]] o Va [[E1]] o app with app = λsf.f<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"> 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<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va-type : Type → Type
<u></u><u></u></span></p>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va-type (x </span>
<span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⇒</span><span style="font-size:12pt;color:black"> x₁) = R</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 ( (Va-type x) </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⇒</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> (Va-type x₁) )<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va-type `</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">ℕ</span><span style="font-size:12pt;color:black">  = R</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 `</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">ℕ</span><span style="font-size:12pt;color:black"><u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va-type (R</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> x)  = R</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 (Va-type x)<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va-type (x </span>
<span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⇒</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> x₁)  = (Va-type x)
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⇒</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> (Va-type x₁)<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va-context : Context → Context<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va-context </span>
<span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∅</span><span style="font-size:12pt;color:black"> =
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∅</span><span style="font-size:12pt;color:black"><u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va-context (x , x₁) =  ( Va-context x , Va-type x₁ )<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va-var : </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∀</span><span style="font-size:12pt;color:black"> {Γ A} → Γ
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∋</span><span style="font-size:12pt;color:black"> A → ((Va-context Γ)
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∋</span><span style="font-size:12pt;color:black"> (Va-type A))<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va-var Z = Z<u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va-var (S x) = S Va-var x<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">And the problematic part is declaring the transform between terms:<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va : </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∀</span><span style="font-size:12pt;color:black"> {Γ A} → Γ
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> A → (Va-context Γ)
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">⊢</span><span style="font-size:12pt;color:black"> (Va-type A)
<u></u><u></u></span></p>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va (` x) = ` Va-var x<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va (ƛ x) =  push</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> (ƛ</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 Va x)<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">-- Here is the hole I cannot come up with filling it<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va {Γ} (x · x₁) = (push</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> (Va x₁))
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;color:black"> ((push</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 (Va x)) </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;color:black"> (ƛ</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 {!!} ))<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va `zero = push</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> `zero<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va (`suc x) = push</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> (`zero) -- paper doesn't provide
 any notion for dealing with sucessors of Nats - currently left like this to pass the typecheck<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">-- Combinators from intermediate language are mapped to itself<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va (push</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> x) = push</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 Va x<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va (ƛ</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black"> x) = ƛ</span><span style="font-size:12pt;font-family:"Segoe UI Symbol",sans-serif;color:black">ₛ</span><span style="font-size:12pt;color:black">
 Va x<u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Va (x </span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;color:black"> x₁) = Va x
</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">∘</span><span style="font-size:12pt;color:black"> Va x₁
<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">The only bit, I am not able to formalise is the "app" combinator, as standard lookup using #_ doesnt work when mapping between terms. <u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">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?<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">I would be most grateful if I could hear back from you!<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black"><u></u> <u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Best,<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12pt;color:black">Wojciech<u></u><u></u></span></p>
</div>
</div>
<p class="MsoNormal">_______________________________________________<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" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><u></u><u></u></p>
</blockquote>
</div>
</div>
<pre>This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.



</pre></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></div>
</blockquote></div></div>