The Coq mailing list

[Yasuaki Kudo <yasu AT yasuaki.com>]

Hi Gabriel and everyone,

 

Thank you so much for your kind replies!   As an admittedly slow student 😊 I really appreciate this – quite often I feel like I am so lost and need to explore various thoughts before I can proceed to the next page of Interactive Theorem Proving and Program Development 😊

 

Your kind replies are very much appreciated and I hope you won’t mind – I will probably ask more questions from time to time 😊

 

Cheers,

Yasuaki

 

 

 

From: Gabriel Scherer
Sent: Sunday, November 15, 2015 7:09 PM
To: Coq Club
Subject: Re: [Coq-Club] Similarities between forall and fun

 

 

On Sun, Nov 15, 2015 at 4:45 AM, Yasuaki Kudo <yasu AT yasuaki.com> wrote:

Although I understand they are different , I wonder, in other languages or other implementations of similar ideas, can these expressions (universal quantification?) be combined as something unified?

 

Just to clarify: there is already a unification between function types and forall quantifications, or equivalently function terms and proofs of forall quantifiers. You are asking for a relation crossing those two level, between a function *term* and a universal quantification (the type).

 

The answer is yes, in two difference senses.

On one hand, I have seen arcane type theories were the two concepts where unified: the type of a lambda-term is a lambda-term (rather than a forall quantification), and you have typing rules like:

  G, x |-  e : t

  --------------------------------

  G |- fun x -> e : fun x -> t

  G |- e : f

  G |- a : t

  ---------------

  G |- e a : f t

 

I don't remember a precise reference, and I always found them not so convincing (I don't see a compelling reason for making this choice, and I suspect they may make those systems harder to use and proof correct, rather than easier).

On the other hand, a classic technique is to factorize any quantifier through a lambda-term (a function). This is what Church introduced lambda-terms for: instead of writing

  forall x, t

  exists x, t

you would apply a function to "forall" and "exists" seen as higher-order functions:

  forall (fun x -> t)

  exists (fun x -> t)

There are works in dependent type theory that use this style, and in my experience it works fine (not very different from the usual style, but that would be a matter of personal taste). Typing rules are then of the form

  G, x |-  e : t

  ------------------------------------------

  G |- fun x -> e : forall (fun x -> t)

  G |- e : forall f

  G |- a : t

  ---------------

  G |- e a : f t

 

This is a common technique in the context of "Logical Frameworks" (systems that strive to have the right feature to make it easy to represent simpler type systems and logics inside them), as you can reuse the meta-level functions (those of the framework) to implement object-level binders (those of the represented system)

(I remember an old article of Thierry Coquand on dependent type theory in this style, but I was unable to find the precise citation.)

 

 

On Sun, Nov 15, 2015 at 4:45 AM, Yasuaki Kudo <yasu AT yasuaki.com> wrote:

Hi,

 

I’m currently studying COQ (well taking a long time…) and have noticed similarities between forall (dependent product?) and function terms.

 

Although I understand they are different 😊, I wonder, in other languages or other implementations of similar ideas, can these expressions (universal quantification?) be combined as something unified?

 

Parameter  F :  nat -> Set .

Parameter  t :  forall x:nat ,  F (1+x) .

Definition t':= fun    x:nat => F (1+x).

 

Check t  1.

Check F  (1+1).

Check t' 1.

 

Regards,

Yasuaki

Tokyo