Email Gateway (Aug 18 2022 at 09:33): Email Gateway (Aug 18 2022 at 09:33):From: paolot@informatik.uni-bremen.de
The following left me puzzled:
consts
lftsnd :: "('a => ('b*'c)) => ('a => 'c)"
funA :: "'a => (('c => 'e)*('d => 'f))"
funB :: "'a => 'h => 'k"
defs
lftsnd_def : "lftsnd f x == snd (f x)"
funB_def : "funB == lftsnd funA"
ô*** Extra type variables on rhs: "'d", "'e"
*** The error(s) above occurred in definition "funC_def":
*** "funC == funB funA"
*** At command "defs".õ
Can anybody spot the problem?
Regards,
Paolo Torrini
Email Gateway (Aug 18 2022 at 09:33):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Paolo,
consts
lftsnd :: "('a => 'b * 'c) => 'a => 'c"
funA :: "'a => ('b => 'c) * ('d => 'e)"
funB :: "'a => 'b => 'c"
defs
lftsnd_def : "lftsnd f x == snd (f x)"
funB_def : "funB == lftsnd funA"
The point is that you don't state anything about the type parameters 'b
and 'c of funA in funB_def since they do not occur on the left hand side
of funB_def; you have to instantiate them:
defs
funB_def : "funB == lftsnd (funA :: 'a => (unit => unit) * ('d => 'e))"
will work.
Hope this helps
Florian
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 09:34):From: Christian Urban <urbanc@in.tum.de>
Florian Haftmann writes:
The point is that you don't state anything about the type parameters 'b
and 'c of funA in funB_def since they do not occur on the left hand side
of funB_def; you have to instantiate them:defs
funB_def : "funB == lftsnd (funA :: 'a => (unit => unit) * ('d => 'e))"
An alternative is to parametrise funB with the types not mentioned.
For example
consts
lftsnd :: "('a => 'b * 'c) => 'a => 'c"
funA :: "'a => ('b => 'c) * ('d => 'e)"
defs
lftsnd_def : "lftsnd f x == snd (f x)"
constdefs
funB_def: "funB TYPE('b) TYPE('c) == lftsnd (funA::'a=>('b=>'c)*('d=>'e))"
The reason why all type-variables of a right-hand side
of a definition have to occur on the left-hand side as
well is that otherwise one can write down definitions
that lead to inconsistencies.
Best wishes,
Christian
Email Gateway (Aug 18 2022 at 09:34):From: paolot@informatik.uni-bremen.de
Quoting Christian Urban <urbanc@in.tum.de>:
Florian Haftmann writes:
The point is that you don't state anything about the type parameters 'b
and 'c of funA in funB_def since they do not occur on the left hand side
of funB_def; you have to instantiate them:defs
funB_def : "funB == lftsnd (funA :: 'a => (unit => unit) *
('d => 'e))"An alternative is to parametrise funB with the types not mentioned.
For exampleconsts
lftsnd :: "('a => 'b * 'c) => 'a => 'c"
funA :: "'a => ('b => 'c) * ('d => 'e)"defs
lftsnd_def : "lftsnd f x == snd (f x)"constdefs
funB_def: "funB TYPE('b) TYPE('c) == lftsnd
(funA::'a=>('b=>'c)*('d=>'e))"
If I parametrise the function, may I instantiate the type parameters
later on, or do I have to bring them with me explicitly all along?
anything in the documentation?
The reason why all type-variables of a right-hand side
of a definition have to occur on the left-hand side as
well is that otherwise one can write down definitions
that lead to inconsistencies.
Do you know if it is generally the case that unistantiated variables lead to
inconsistencies? I mean, take something like
consts
consA :: "('a*bool)"
constdefs
consB_def : "consB == snd consA"
I was just wondering how one may get an inconsistency from there.
Cheers,
Paolo
Email Gateway (Aug 18 2022 at 09:34):From: Stefan Berghofer <berghofe@in.tum.de>
paolot@informatik.uni-bremen.de wrote:
Do you know if it is generally the case that unistantiated variables
lead to inconsistencies?
If you were allowed to make the following definition
singleton :: bool
"singleton == (ALL (x::'a) (y::'a). x = y)"
which has an extra type variable 'a on the right-hand
side, you could derive
True =
(ALL (x::unit) (y::unit). x = y) =
singleton =
(ALL (x::bool) (y::bool). x = y) =
False
which is an inconsistency.
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 09:34):From: Stefan Berghofer <berghofe@in.tum.de>
paolot@informatik.uni-bremen.de wrote:
If you define consA as follows
consA == (arbitrary::'a, ALL (x::'a) (y::'a). x = y)
which is a perfectly legal definition, since 'a occurs
both on the left-hand and on the right-hand side, you
could still derive an inconsistency in a similar way
by using the (illegal) definition of consB.
Greetings,
Stefan
Inconsistency.thy
Email Gateway (Aug 18 2022 at 09:34):From: paolot@informatik.uni-bremen.de
Quoting Stefan Berghofer <berghofe@in.tum.de>:
ok, thanks. Still, the example I had in mind was:
consts
consA :: "('a*bool)"
constdefs
consB_def : "consB == snd consA"
I'd expect the following is logically safe:
ALL x::singleton. snd (x,y) = ALL x::bool. snd (x,y)
The extra type variable is there, but it is simply not used.
Best,
Paolo
Last updated: May 03 2024 at 12:27 UTC