Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Axioms of parametricity?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axioms of parametricity?


chronological Thread 
  • From: Taral <taralx AT gmail.com>
  • To: "Matthieu Sozeau" <Matthieu.Sozeau AT lri.fr>
  • Cc: "Coq Club" <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Axioms of parametricity?
  • Date: Wed, 19 Nov 2008 10:06:02 -0800
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=TdDmPJri5lfy3/RRECR3JaBWnE5mbOMO0Q/OJ6UJXxUObYhBPBJ9HWbxFUN+s9Iy/Q 70uFiUK80dE0FAui6Dv0lM2utELFlvAObFgaDI2mkFOSGpDNczVzMNJWykTKiTr7lrGq ij7PjE08pzd+3lcBN2TvHkt/FhaMstAwen30Q=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Wed, Nov 19, 2008 at 2:05 AM, Matthieu Sozeau 
<Matthieu.Sozeau AT lri.fr>
 wrote:
> By instantiating this with the trivial relation (fun x y : T, True), you 
> get that
> [forall x y, f T x = f T y].
> I believe this is not provable for any variable [f] of type [forall T, T -> 
> Test] but
> by a parametricity theorem any instance for some concrete [f] should be
> derivable.

Very interesting. In effect, Coq does not have (can not have?) a
parametricity axiom for its own functions, even though parametricity
is provable for any given concrete function. Lessons of the day: 1.
Get the Coq'Art book. 2. Read the "Theorems for free" papers.

Thanks everyone so far. Any further ideas are welcome.

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown



Archive powered by MhonArc 2.6.16.

Top of Page