[Agda] How can I implement naive sized lambdas?
Georgi Lyubenov
godzbanebane at gmail.com
Tue Mar 24 23:28:16 CET 2020
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200325/d680a176/attachment.html>
More information about the Agda
mailing list