[Agda] Converting intrinsically typed terms

[rozowski w.k. (wkr1u18)]

Hello Everyone!

Thank you so much for your reply!

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!

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!

3) Wouter - The paper I am formalising is https://www.cs.tufts.edu/comp/150FP/archive/remi-douence/functional-vms.pdf - 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: https://gist.github.com/wkr1u18/e32b670ce50b4ee248f7c72e80123b29) - I tried extrinsically typed version following the PLFA formalism ( here is what I have so far https://gist.github.com/wkr1u18/97ce47d221fc30b1f40c7e26b69eecd9), so I could separately define the transform on the terms and then prove the welltypedness of the transform.

Best,
Wojciech

________________________________
From: Swierstra, W.S. (Wouter) <W.S.Swierstra at uu.nl>
Sent: 06 November 2020 07:30
To: rozowski w.k. (wkr1u18) <wkr1u18 at soton.ac.uk>; agda at lists.chalmers.se <agda at lists.chalmers.se>
Subject: Re: Converting intrinsically typed terms

CAUTION: This e-mail originated outside the University of Southampton.

Hi Wojciech,

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.

Good luck with your project!

  Wouter

________________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of rozowski w.k. (wkr1u18) <wkr1u18 at soton.ac.uk>
Sent: Monday, 2 November 2020 11:55
To: Agda users
Subject: [Agda] Converting intrinsically typed terms

Hello everyone!

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.
I am writing to ask for any advice how to formalise type correct transformations between intrinsically typed terms.

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.

The type rules (and way of building terms - because intrinsic typing) for those combinators, are:
  pushₛ_ : ∀ {Γ A}
    → Γ ⊢ A
      -----
    → Γ ⊢ Rₛ A

  ƛₛ_  : ∀ {Γ A B}
    → Γ , A ⊢ B
      ---------
    → Γ ⊢ A ⇒ₛ B

  _∘_ : ∀ {Γ A B}
    → Γ ⊢ Rₛ A
    → Γ ⊢ A ⇒ₛ B
      ---------
    → Γ ⊢ B

(Rs A is just annotated type for something of type A being stored on stack)

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:

  ξ-∘ₛ₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ₛ B} {M : Γ ⊢ Rₛ A}
    → L —→ L′
      ---------------
    → M ∘ L —→ M ∘ L′

  ξ-∘ₛ₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ₛ B} {M M′ : Γ ⊢ Rₛ A}
    → Value V
    → M —→ M′
      ---------------
    → M ∘ V —→ M′ ∘ V

  β-∘ₛ :  ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
      -------------------
    →  (pushₛ W) ∘ (ƛₛ N) —→ N [ W ]

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:

Va : Λ→Λs

Va [[x]] = pushs x
Va [[λx.E]] = pushs (λsx.Va [[E]] )
Va [[E1 E2]] = Va [[E2]] o Va [[E1]] o app with app = λsf.f

 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

Va-type : Type → Type
Va-type (x ⇒ x₁) = Rₛ ( (Va-type x) ⇒ₛ (Va-type x₁) )
Va-type `ℕ  = Rₛ `ℕ
Va-type (Rₛ x)  = Rₛ (Va-type x)
Va-type (x ⇒ₛ x₁)  = (Va-type x) ⇒ₛ (Va-type x₁)

Va-context : Context → Context
Va-context ∅ = ∅
Va-context (x , x₁) =  ( Va-context x , Va-type x₁ )

Va-var : ∀ {Γ A} → Γ ∋ A → ((Va-context Γ) ∋ (Va-type A))
Va-var Z = Z
Va-var (S x) = S Va-var x

And the problematic part is declaring the transform between terms:

Va : ∀ {Γ A} → Γ ⊢ A → (Va-context Γ) ⊢ (Va-type A)
Va (` x) = ` Va-var x
Va (ƛ x) =  pushₛ (ƛₛ Va x)

-- Here is the hole I cannot come up with filling it
Va {Γ} (x · x₁) = (pushₛ (Va x₁)) ∘ ((pushₛ (Va x)) ∘ (ƛₛ {!!} ))
Va `zero = pushₛ `zero
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

-- Combinators from intermediate language are mapped to itself
Va (pushₛ x) = pushₛ Va x
Va (ƛₛ x) = ƛₛ Va x
Va (x ∘ x₁) = Va x ∘ Va x₁

The only bit, I am not able to formalise is the "app" combinator, as standard lookup using #_ doesnt work when mapping between terms.
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?

I would be most grateful if I could hear back from you!

Best,
Wojciech
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201106/cc5d60b3/attachment.html>