Discussion:
Encoding higher lambda calculus in agda
Add Reply
How Si Yu
2018-04-05 02:36:21 UTC
Reply
Permalink
Raw Message
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
Jason -Zhong Sheng- Hu
2018-04-05 03:01:58 UTC
Reply
Permalink
Raw Message
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-***@lists.chalmers.se> on behalf of How Si Yu <***@gmail.com>
Sent: April 4, 2018 10:36:21 PM
To: ***@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
András Kovács
2018-04-05 06:33:04 UTC
Reply
Permalink
Raw Message
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.

Predicative dependent type theories can be represented and proven
consistent; this is <http://www.cse.chalmers.se/~abela/popl18.pdf> the most
advanced development I know of which only uses native Agda features (in
this case, induction-recursion). Note though that formal handling of
dependent types tends to be highly technically challenging.

For dependent type itself, I do not think it's possible, due to Goedel's
Post by Jason -Zhong Sheng- Hu
incompleteness theorem.
Gödel doesn't enter the picture in any of the developments I know of,
because the metatheories are stronger than object theories, due to having
inductive families and/or induction/recursion. Also, Gödel would only
prevent consistency proofs, but doesn't preclude representing the syntax or
doing a number of interesting things with it which don't imply consistency.

is Prop type in Coq is impredicative, and therefore the calculus underneath
Post by Jason -Zhong Sheng- Hu
(caculus of inductive constructions, CIC) is stronger than calculus of
constructions(CoC)
CoC has impredicative base Set.
Post by 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).
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 ht
tps://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*
------------------------------
*Sent:* April 4, 2018 10:36:21 PM
*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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Henning Basold
2018-04-05 08:15:57 UTC
Reply
Permalink
Raw Message
Hi,
Post by András Kovács
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.
How Si Yu
2018-04-05 08:18:31 UTC
Reply
Permalink
Raw Message
Thanks for the links. Looking at
https://github.com/sstucki/system-f-agda/blob/master/src/SystemF/WtTerm.agda
,
data _⊢_∈_ {m n} (Γ : Ctx m n) : Term m n → Type n → Set where
I get why I was stuck because I was thinking along the line of
data _⊢_ {m n} (Γ : Ctx m n) : Type n → Set where

which tries to make only well-typed term constructible instead of
constructing terms then prove some of them are well-typed.
except for dependent type itself(i.e. the strongest calculus of the cube).
By dependent type, do you mean COC? Usually one talks about dependent
type, I'm expecting anything that is at least as strong as λP.
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.
Predicative dependent type theories can be represented and proven
consistent; this is <http://www.cse.chalmers.se/~abela/popl18.pdf> the most
advanced development I know of which only uses native Agda features (in
this case, induction-recursion). Note though that formal handling of
dependent types tends to be highly technically challenging.
For dependent type itself, I do not think it's possible, due to Goedel's
Post by Jason -Zhong Sheng- Hu
incompleteness theorem.
Gödel doesn't enter the picture in any of the developments I know of,
because the metatheories are stronger than object theories, due to having
inductive families and/or induction/recursion. Also, Gödel would only
prevent consistency proofs, but doesn't preclude representing the syntax or
doing a number of interesting things with it which don't imply consistency.
is Prop type in Coq is impredicative, and therefore the calculus underneath
Post by Jason -Zhong Sheng- Hu
(caculus of inductive constructions, CIC) is stronger than calculus of
constructions(CoC)
CoC has impredicative base Set.
Post by 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).
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 ht
tps://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*
------------------------------
*Sent:* April 4, 2018 10:36:21 PM
*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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Loading...