Email Gateway (Aug 19 2022 at 12:37): Email Gateway (Aug 19 2022 at 12:37):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
This is the result of my making comparisons between Scala and Haskell.
I'd like to generate a little code for whatever I'm doing, and messing
around with the meta-logic is something I eventually want to do. It
could be I'm doing things which aren't intended to be done.
I start with a hybrid version of "not" named "Hnot", (PROP P ==> False),
and I export it.
definition MFalse :: "prop" ("MFalse") where "MFalse == (!!P. PROP P)"
definition Hnot :: "prop => prop" where "Hnot P == (PROP P ==> False)"
value "Hnot(Trueprop False)"
export_code Hnot in Scala file "i131123a.scala"
export_code Hnot in Haskell file "."
I actually wanted to use "(PROP P ==> MFalse)", but MFalse uses "!!", so
I get the export_code error message "No code equations for all".
QUESTION: Are there some magic code equations for "all", or is this a
fundamental limitation?
Starting here, I make some comments about the Haskell code, since it's
almost like reading the Isar.
From the generated code, HOL "prop" is converted to a data type "Prop",
which has only one value, "Holds".
data Prop = Holds;
I guess it makes sense that "Prop" can only be true, but consequently,
it makes the use of variables in "follows", the meta-implication, rather
meaningless:
follows :: Prop -> Prop -> Prop;
follows p Holds = Holds;
follows Holds p = p;
I set that aside because the use of HOL is the main objective for most
people. This brings us to "trueprop", which is the code for "Trueprop".
trueprop :: Bool -> Prop;
trueprop True = Holds;
This shows that "trueprop" is only defined for "true". I set that aside,
as a solitary issue, and talk about "hnot", which seems like it should
be a valid function:
hnot :: HOL.Prop -> HOL.Prop;
hnot p = HOL.follows p (HOL.trueprop False);
Here, I've reached the limits of knowing what the limits of code
generation is supposed to be, when it comes to the meta-logic.
In Isabelle I can do this, and I get a value of True:
value "Hnot(Trueprop False)"
I'm actually using the Scala code to test the functions in simple ways,
and I can't do that. The function "trueprop" is not defined for "false",
so both "trueprop" and "hnot" throw an exception.
This is kind of contrary to the following four statements in HOL.thy,
where, by necessity, Trueprop is defined for both True and False:
typedecl bool
Trueprop :: "bool => prop"
consts
True :: bool
False :: bool
As I said, it could be that none of this was intended to be used like this.
Thanks,
GB
theory i131123a
imports Complex_Main
begin
definition MFalse :: "prop" ("MFalse") where
"MFalse == (!!P. PROP P)"
definition Hnot_try :: "prop => prop" where
"Hnot_try P == (PROP P ==> MFalse)"
export_code Hnot_try in Scala file "i131123a.scala"
(ERROR: No code equations for all)
definition Hnot :: "prop => prop" where
"Hnot P == (PROP P ==> False)"
value "Hnot(Trueprop False)"
export_code Hnot in Scala file "i131123a.scala"
export_code Hnot in Haskell file "."
end
i131123a.thy
Email Gateway (Aug 19 2022 at 12:39):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Code generation has been an excellent tutor. Seeing "data prop Holds" by
the code generator has drove home a simple idea, that I can never make a
false statement at the prop level of logic. Sounds simple, but until
now, I've always consider true and false to both be available to me.
However, my "hnot(false)" doesn't attempt to make a false statement. It
makes the statement "False ==> False", which is true, and so it
shouldn't throw an exception.
I don't know if this is good enough for the future, but for the moment,
I made "trueprop" part of the "prop" data type, and defined "follows" so
that an exception is thrown there when a false meta-implication is
attempted.
The Scala objects below, "HOL2" and "HOL" are a combination of the Scala
objects that were exported for the source in my last email. "HOL2" is my
modification.
If one says, "Is not an exception thrown semantically equivalent to a
meta-logic false?" I reply, "I know nothing about semantics or
predicates. Those computer scientists, that is what they talk about, but
me, I know nothing about semantics or predicates."
Regards,
GB
// FIXED FOR NOW, MAYBE.
object HOL2 {
sealed abstract class prop
final case class Holds() extends prop
final case class trueprop(x0: Boolean) extends prop
// ECLIPSE WARNING: match may not be exhaustive. It would fail on the
// following input:
// (trueprop(true), trueprop(false))
// Dude, exactly, it's impossible to make a false statement at the prop
// level of logic. Exceptions are acceptable, but meta-logic false is
// semantically offensive to those in the know.
def follows(p: prop, pa: prop): prop = (p, pa) match {
case (p, Holds()) => Holds()
case (Holds(), trueprop(true)) => Holds()
case (trueprop(false), trueprop(true)) => Holds()
case (trueprop(true), trueprop(true)) => Holds()
case (trueprop(false), trueprop(false)) => Holds()
}
def hnot(p: prop): prop = follows(p, trueprop(false))
// Return value of Holds(). It's legit, is it not?
val x = hnot(trueprop(false))
// No error. Simple assignment. I'm not making any logical claim.
val y = trueprop(false)
// Throws exception. Not because or "trueprop", but because of
"follows".
// That's what I want for now. Concerning the future, maybe not.
val z = hnot(trueprop(true))
}
// ORIGINAL: THROWS EXCEPTION FOR A LEGIT STATEMENT.
object HOL {
sealed abstract class prop
final case class Holds extends prop
def trueprop(x0: Boolean): prop = x0 match {
case true => Holds()
}
def follows(p: prop, pa: prop): prop = (p, pa) match {
case (p, Holds()) => Holds()
case (Holds(), p) => p
}
def hnot(p: prop): prop = follows(p, trueprop(false))
// Throws exception. This is not where it should throw the exception,
because
// hnot(false) should be an acceptable statement.
val x = trueprop(false)
}
i131123a__mod_to_throw_exception_at_follows.scala
Email Gateway (Aug 19 2022 at 12:41):From: Gottfried Barrow <gottfried.barrow@gmx.com>
This is my last email on this, unless someone wants to straighten me out
on anything, but in about 2 to 3 months from now, I'm going to start
trying to use the concept that I outlined in last email, where I made an
attempt to fix the exception problem, unless someone wants to explain
why I'm off track.
Its taken me a while to get to the code generator, where I specifically
learned about "export_code" from a tip given to me here several weeks
ago by Florian. It pays to ask questions, and get a tip here and there
for some of them.
There are "huge" parts of Isabelle, and I'll now put the code generator
in with those huge parts, like Isar as a high-level language, the
meta-logic of Pure, the object logic of HOL, Sledgehammer, the PIDE
interface, and other auto tools.
Complements from a mere user are now out of the way.
Here, I'm thinking about whether "prop" and "==>" are supposed to get
their meaning from their use with "value" or from their use with
"theorem". I guess I'm stating the obvious in saying that Isabelle/Pure
can't be exported as about 10 lines of Scala or Haskell code, and so
something has to be lost.
Essentially, "value", which I understand is related to the code
generator, doesn't return a "prop" value of "so-called-meta-true" or
"so-called-meta-false", as shown by these examples:
value "True ==> False" (* returns (Trueprop False)::prop *)
value "False ==> True" (* returns (Trueprop True)::prop *)
value "!!P. PROP P" (* returns (!!u::prop. PROP u)::prop *)
The short story is that the Haskell line of code "data prop Holds" is my
guiding principle, and that the meaning of "prop" and "==>" should come
from "theorem" and not "value", otherwise, the meta-logic, when
exported, will be no different from the object logic (which may be
inescapable). That's the way it appears to me.
I look to the software to teach me logic. I look to it to give me, as an
enforcer, the years of knowledge the programmers have, who have written
the software.
When the software doesn't give me strict guidance, I'm willing to get
creative, but I'd rather waste less of of my time than more of it by
going off track.
Regards,
GB
Email Gateway (Aug 19 2022 at 12:44):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gottfried,
the trick of the definition "holds == Trueprop True" and the related
stuff is just used to allow the code generator (code_runtime.ML) to
evaluate expressions of the form (P) "Trueprop _" and check whether they
result in "Trueprop True" aka "holds" and then certify the result as
theorem (P). It has no further significance.
Maybe this answers you abundant questions.
Cheers,
Florian
Email Gateway (Aug 19 2022 at 13:10):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Exposure to tricks can still result in light-bulb moments. It's more
clear to me now that an expression likevalue "!!P. PROP P" and value
"Trueprop False" never get simplified to some meta-logic false
constant. I take that as meaning there is no meta-logic false that's
been defined. If there is, maybe someone will tell me where it is.
I guess no one but me cares about exporting functions of type "prop =>
prop" and "prop => prop => prop".
I decided that Scala "val" should mimic Isar "value" with functions
based on type prop.
It should produce something that looks like these:
value "True" (* True::bool *)
value "False" (* False::bool *)
value "Trueprop True" (* (Trueprop True)::prop *)
value "Trueprop False" (* (Trueprop False)::prop *)
value "hNot(True)" (* (Trueprop False)::prop *)
value "hNot(False)" (* (Trueprop True)::prop *)
In the exported code, I changed "trueprop" from a function to a datatype
and got rid of "Holds". Until the day I can figure out how to export
"!!P. PROP P", or "(op ==>) == (op &&&)", I don't see a need for it, but
I could be wrong.
Based on my limited knowledge, I think the modified "trueprop" and
"follows" should work as a drop-in replacement for any exported
functions of type "prop => prop => prop".
Thanks,
GB
// Modification to get Scala "val" to work like Isar "value"
object I_131123b_mod {
abstract sealed class prop
final case class trueprop(b: Boolean) extends prop
def follows(p: prop, pa: prop): prop = (p, pa) match {
case (p, trueprop(true)) => trueprop(true)
case (trueprop(false), trueprop(false)) => trueprop(true)
case (trueprop(true), trueprop(false)) => trueprop(false)
}
def hNot(p: prop): prop = follows(p, trueprop(false))
val x1 = true // x1: Boolean = true
val x2 = false // x2: Boolean = false
val x3 = trueprop(true) // x3: trueprop = trueprop(true)
val x4 = trueprop(false) // x4: trueprop = trueprop(false)
val x5 = hNot(trueprop(true)) // x5: prop = trueprop(false)
val x6 = hNot(trueprop(false)) // x6: prop = trueprop(true)
// HOL functions (bool => bool) are just Scala (Boolean => Boolean).
def bNot(b: Boolean): Boolean = !b
} /* object I_131123b */
theory i131123b__scala_val_should_match_isa_value
imports Complex_Main
begin
definition hNot :: "prop => prop" where
"hNot P == (PROP P ==> False)"
notation hNot ("hNot _" [5] 5)
value "True" (* True::bool *)
value "False" (* False::bool *)
value "Trueprop True" (* (Trueprop True)::prop *)
value "Trueprop False" (* (Trueprop False)::prop *)
value "hNot(True)" (* (Trueprop False)::prop *)
value "hNot(False)" (* (Trueprop True)::prop *)
theorem "hNot(False)"
by(unfold hNot_def, simp)
definition bNot :: "bool => bool" where
"bNot b = (~b)"
no_notation hNot ("hNot _" [5] 5)
export_code hNot bNot Not in Scala module_name "I_131123b" file
"i131123b.scala"
end
// ORIGINAL EXPORT
object I_131123b {
abstract sealed class prop
final case class Holds() extends prop
def trueprop(x0: Boolean): prop = x0 match {
case true => Holds()
}
def follows(p: prop, pa: prop): prop = (p, pa) match {
case (p, Holds()) => Holds()
case (Holds(), p) => p
}
def bNot(b: Boolean): Boolean = ! b
def hNot(p: prop): prop = follows(p, trueprop(false))
} /* object I_131123b */
Last updated: Nov 21 2024 at 12:39 UTC