Email Gateway (Aug 19 2022 at 16:54): Email Gateway (Aug 19 2022 at 16:54):From: Gottfried Barrow <igbi@gmx.com>
Hi,
I have a question for the Big Guns, and I posted it on Stackoverflow:
It's big enough to where I want to increase the chances that I'll either
get an answer in the negative, an answer that's complete enough for me
to finish it, or an answer that's a plain ole, complete working solution.
There is the UGB, the universal set of Isabelle/HOL Big Guns, and a
subset of UGB, the BGAOSO, the Big Guns Active on Stackoverflow. Members
of the BGAOSO have actually been very helpful, and I've gotten important
answers on SO. For anything important, it seems like it was answered.
I think SO is a better staging place for a more involved question, one
where there's a good chance it won't get answered, or won't get answered
with enough detail for me to finish the job.
If the answer is deceptively simple, that would not be bad. Within the
scope of that which is called bad, compared to that which is called
good, it, a deceptively simple answer, would be of that quality which is
commonly called good, or, simply, good.
It's okay if it's answered here. If it's answered here and not there,
I'll probably delete the question there. I could include it all here,
now, but the formatting is better there, so it seems I should leave it
all there, at this time.
Thanks,
GB
Email Gateway (Aug 19 2022 at 16:54):From: Gottfried Barrow <igbi@gmx.com>
I get impatient, so that question I was asking about is gone, or soon
will be.
I'll give you something of importance that I said there, which is the
Law of df&P:
(The Law of df&P): There is pattern matching with datatype and fun, let
it not escape your use.
I like things black and white, so I need laws to work by. I now have a
new one, which is the result of eliminating some complexity, and
accepting a compromise.
(The Law of the Universe Plus One): There is 'a option, use it directly,
in it's simple brilliance.
I was using it, but not in its simplicity, because I was trying to solve
a problem that comes, at least partly, from the limitations of simple
types. Given a fundamental type, like nat, ideally, defining a new type,
such as that n = 1 or n = 7, should be a one-liner, but things end up
getting complicated.
I looked at the standard example of a dependent type to try and get a
bare minimum understanding. I don't know whether dependent types would
even solve the problem above, because, as far as I can tell, if I don't
restrict the domain of a type with the use of type constructors, rather
than with a predicate, it doesn't help. The end result can be that I
just introduce a lot of complexity, trying to achieve an idea, that my
domain should be encoded in my type name.
Why I don't switch to dependent types? I would. I'm a fair weather
friend when it comes to proof assistants.
What I do is try to do is get a glimpse of what I don't understand, and
make decisions on my glimpse, because understanding takes times. My
glimpse tells me that complexity comes at a cost. Limitations force me
to seek simpler solutions, or to deal with details directly, and when I
deal with details directly, I'm probably closer to what the hardware
really does, and the details, again, make me seek simpler, more
straightforward solutions. There are lots of things to consider, though.
Here's a brilliant use of None:
instantiation option :: ("numeral") numeral
begin
definition one_option :: "'a option" where
"one_option == Some 1"
definition plus_option :: "'a option => 'a option => 'a option" where
"x + y == if x = None | y = None then None else Some (the x + the y)"
declare plus_option_def [simp add]
instance by(default, auto simp add: add.assoc)
end
declare [[coercion "Some :: nat => nat option"]]
And someone says, "Nothing new, guy, I've been using that for quite a
long time." And I was hoping to hear that, because I need someone to
appreciate my brilliant use of None.
Okay, because no one answered the question I requested help with, I want
to ask for help on something else.
I need to know which of two phrases is grammatically correct. Should I
say, "None is brilliant" or "None are brilliant"? Puns, yes, I would
like to ask about those too, but I can ask about those later.
I said I'm impatient, right? Yes, I did. People, if they don't help me,
I have to figure things out for myself, or look for another solution.
"None". It's polymorphic, is it not? Okay, then it's "are".
I think I've got a glimpse that the use of "None" has some good set
theoretical zemantics. Sometimes it's the universe, and sometimes it's a
set complement.
As to the sematics of zemantics, that's paying homage to the fact that
in all my formal education, I don't remember once hearing a
mathematician use the word "semantics".
Is that a complaint? Not at all, because I don't need semantics and I
don't understand formal semantics. It also doesn't end up being a
limitation, because I don't design languages, I use languages that. Why
should I use the word?
I had truth tables, and now I have syntax. Semantics? No, I have no need
for semantics, not when I have syntax and zemantics. One string of
characters goes in and another string of characters comes out. How do I
know? Because, I can see it all, in the console, that's why I keep it
open all the time.
As to the zemantics of that little house in the console, and maybe even
its semantics, I'm not sure. Maybe it's saying, "Hey, you, logical wimp,
why you using Sledgehammer so much? Maybe I'll kick your logical tail,
and send you home."
That I don't use semantics, does that mean I don't need interpretation?
No, of course I need interpretation, even with zemantics at my disposal.
I look in the console. What do I see? An "x". Then, later on, not an
"x", but an "x::'a". Later on even, not an "x::'a", but an
"x::'a::numeral". This requires syntactic interpretation, that "x", I
need to interpret it as "x::'a", and further, that "x::'a", it should be
interpreted as "x::'a::numeral". I work it out again, to make sure I'm
right. One character went in. Fourteen characters came out. I interpret
it all again. Even a third time. Finally, I'm convinced that "x", yea,
it's exactly the same "x" as "x::'a", which is exactly the same "x::'a"
as "x::'a::numeral". Well, somehow not "exactly the same", but that's
the benefit of zemantics over semantics. With zemantics, you don't sweat
the small stuff.
Regards,
GB
Last updated: Apr 18 2024 at 16:19 UTC