[Agda] Encoding higher lambda calculus in agda

[Jason -Zhong Sheng- Hu]

my intuition was there is nothing special about system F, and all terms and types should be just able to fit into Set along. and indeed, someone has done the work: https://github.com/sstucki/system-f-agda


regarding stronger calculus, i do not see why they are not possible, except for dependent type itself(i.e. the strongest calculus of the cube). For example, it's straightforward to formalize Fsub in Coq: https://github.com/plclub/metalib/tree/master/Fsub


The modelling calculus of Scala, (dependent object types, DOT), for example, has type dependent types, type dependent values, and a weak form of value dependent types, which can also be proved with terms and types in Set: https://github.com/samuelgruetter/dot-calculus https://github.com/amaurremi/dot-calculus


Though in Coq, the terms and types are defined in Set, which roughly corresponds to Set in Agda, and that hopefully means you won't need to go above Set 2 to prove it's sound.


For dependent type itself, I do not think it's possible, due to Goedel's incompleteness theorem. However, someone did it in Coq (which i've not checked, but, well, it's there) https://github.com/coq-contribs/coq-in-coq . The reason why it might be doable in Coq, is Prop type in Coq is impredicative, and therefore the calculus underneath (caculus of inductive constructions, CIC) is stronger than calculus of constructions(CoC). Indeed, the author represents typ to be Prop because he had no choice. https://github.com/coq-contribs/coq-in-coq/blob/master/Types.v


Hope that helps.


Sincerely Yours,

Jason Hu
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of How Si Yu <howseeu at gmail.com>
Sent: April 4, 2018 10:36:21 PM
To: agda at lists.chalmers.se
Subject: [Agda] Encoding higher lambda calculus in agda

Hi,

There are numerous implementations of untyped lambda calculus and
simply typed lambda calculus in Agda online. However, I can't find any
mention of encoding of other "higher" lambda calculus in the lambda
cube like λ2 or λP in Agda. Is it because they are inherently
impredicative and can't be represented in Agda?

Thanks,
Si Yu
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180405/58947a75/attachment.html>