[Agda] Encoding higher lambda calculus in agda

[Henning Basold]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Hi,

On 05/04/18 08:33, András Kovács wrote:
> 
> You can represent the syntax of pretty much every dependent and 
> impredicative theory in Agda. However, that does not settle whether
> a particular proof or construction using a syntax is a) possible in
> base Agda b) feasible or convenient in base Agda.
> 
> System F and F-omega syntax is easy to represent in Agda, in
> either intrinsic or extrinsic manner. Showing consistency or
> normalization would require an impredicative universe in Agda, so
> that's not possible without postulating stuff, but even without
> that there are many interesting things which you could do with the
> syntax.
> 

In fact, this applies to almost any type theory, because standard
normalisation proofs are often impredicative, even for simple type
theories. For an example of a predicative encoding of such a proof
see, for example, [AA99].

As for the formalisation of dependent types in Agda: The main
difficulty is the fact that the typing judgement involves the
reduction relation of the theory, which leads to trouble especially
with recursive types. One technique to overcome this is to define
pre-terms, which are untyped terms or terms that have only
informations about arities of constructors etc. In [Geu94], a strong
normalisation proof is given, where the reduction relation is given in
such a way. I used an extension of that technique to encode a
dependent type theory of inductive-coinductive types in Agda
(https://github.com/hbasold/CoindDepTypes). Finally, people have
recently started to use higher inductive types to define the term
equalities by using propositional equality rather by using reduction
relations, see the thesis of Ambrus Kaposi [Kap17].

Best,
Henning

[AA99] Abel, Andreas, and Thorsten Altenkirch. 1999. ‘A Predicative
Strong Normalisation Proof for a Lambda-Calculus with Interleaving
Inductive Types’. In TYPES’99, edited by Thierry Coquand, Peter
Dybjer, Bengt Nordström, and Jan M. Smith, 1956:21–40. LNCS. Springer.
https://doi.org/10.1007/3-540-44557-9_2.

[Geu94] Geuvers, Herman. 1994. ‘A Short and Flexible Proof of Strong
Normalization for the Calculus of Constructions’. In Types for Proofs
and Programs, edited by Peter Dybjer, Bengt Nordström, and Jan Smith,
14–38. LNCS 996. Springer Berlin Heidelberg.
https://doi.org/10.1007/3-540-60579-7_2.

[Kap17] Kaposi, Ambrus. 2017. ‘Type Theory in a Type Theory with
Quotient Inductive Types’. University of Nottingham, UK.
http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.713896.
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlrF2zkACgkQatBsEc2x
Mm6y6w/+PUUbSZURaVySXKJ9iu+jD9QvNQEftvyzp7OZpjopwesiXAEvwSeLy4VJ
wCLVTPAVAjyTzZXxwrCtNAqvHv9ql1L8/42a4o5bU23QbIbV1s5hVQ8GP+gSUpJD
+0edLiD0vvROlvKlfnLWhPDpzcL7yFZiGfYgNLRw7nA6k0V7DzXPcBwch/JbMy2w
i6KR9ZNKqLwLEXoFn32cgaZKWHBVj++ePiAiXs1wNyvfXVfzHnuQfi5fwj4CzmqL
h7X7sf2Jp7GNLABstLk1pD7ce94P1d+bLslHr9P5sAYk/ApgBhgKaH+6AB2rR2U8
yK1UZNrACAcxq7Q3QnE9VXH/vpA8DnHDzOmBnhMLfkFSn+w4J4jE93xVjps258QV
kvea3PVw0qiIW+Ev3UB3GtEkfYhu1D8yzWyLh81nPCHqg3c8giUNSzZVAEPVG+4m
wn/iYsBK43vRAY6+WBLESQ1hMbCTRdyP/HvkdvCSSTQk6/1X269X+i8U732+BLdF
Flr3ETTXq947vsq9SffW2aYEGBrhilU8p+LEyDVP5/OTTAcyHm7NceYVUcTVX28W
ojQP0Tp/47+6alBnyqrXiwfu3pzJbFuCN+dkk9dlmXlmiXtntJeXP8HmlTm0M+XR
MTWqiztovRe1qMZSx0cAS3PW/XVG5+9z1YTdmKcvLQGcBoHO+o8=
=AxEr
-----END PGP SIGNATURE-----