[Agda] How can I implement naive sized lambdas?
Guillaume Allais
guillaume.allais at ens-lyon.org
Wed Mar 25 11:09:57 CET 2020
Hi Georgi,
I would advise against working directly with raw names: you get
absolutely no support from the typechecker to enforce well-scopedness
and it is very easy to shoot one's foot off.
This warning out of the way, this is the type signatures I would
start with:
* Not using `Size<` (that works well with codata, not with data)
* Giving subterms the *same* size (a size is an upper bound anyway)
* Giving the return type a size increased by one (using `↑_`)
=====================================================================
open import Size
open import Data.Nat.Base
variable
i : Size
data Lam : Size → Set where
var : ℕ → Lam (↑ i)
app : Lam i → Lam i → Lam (↑ i)
lam_>_ : ℕ → Lam i → Lam (↑ i)
ren : (ℕ → ℕ) → Lam i → Lam i
ren = ?
sub : (ℕ → Lam ∞) → Lam i → Lam ∞
sub = ?
=====================================================================
Best,
gallais
On 24/03/2020 22:28, Georgi Lyubenov wrote:
> Hello!
>
> Sorry if this isn't the right place to ask a question like this!
>
> I want to express named lambda terms in Agda. By doing so in the most
> "naive" way possible, I encounter a termination issue when implementing
> substitution - when I want to rename a variable to avoid accidental
> variable capture, the termination checker is unhappy - I'm trying to do a
> recursive call (recursive calling substitution) on the result of a function
> (renaming). My first thought is to attach sizes (via either Nats or the
> builtin Size type), and show that renaming doesn't "change size". After a
> bit of struggling I couldn't manage to do so, and am writing to ask for a
> hint or some advice.
>
> This is my initial attempt:
>
> data : Size -> Set where
> v : {i : Size} -> (n : Nat) -> Lambda i
> _app_ : {i j : Size} -> Lambda i -> Lambda j -> Lambda (sizeSuc (sizeMax
> i j))
> lam_>_ : {i : Size} -> Nat -> Lambda i -> Lambda (sizeSuc i)
>
> but with this I can't even implement something like
>
> promo : {i j : Size} -> Lambda i -> Lambda (sizeMax i j)
>
> Furthermore I have no idea what return type to even give to substitution!
>
> I am pretty sure I am missing something very fundamental about sizes and
> how to use them, but I couldn't find materials to answer my question.
>
> Thanks in advance!
>
> =======
> Georgi
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
More information about the Agda
mailing list