[Agda] How can I implement naive sized lambdas?
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Mar 27 03:44:12 CET 2020
Hello Georgi,
you already received some good advice. In general, I second Andras'
advice to first define renaming and then (parallel) substitution. If
you want to do it in one definition, you can use Conor McBride's trick:
http://www.cse.chalmers.se/~abela/html/ParallelSubstitution.html
(See http://www.cse.chalmers.se/~abela/projects.html for some more code
snippets.)
The blog post by Rob Simmons is neat, but I'd say not entirely state of
the art; you definitely want parallel substitution as the primitive, not
single substitution as Rob defines it (maybe owned to the fact that he
comes from a Twelf background).
Cheers,
Andreas
On 2020-03-24 23: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