BooleanAlgebrasIntro2 - News
posted by deluger, Mon 16 Jan 2023 04:13:59 AM UTC
I always feel uncomfortable without a background C development.
So, now that there's something too Sturm und Drang about a Boolean CAS, how about applied term algebras!
The good news is I have a simpler specification and interface (boyoboy); words (in a free semigroup) are easier to deal with than bits and whatnot (or at least the way
[...]
posted by deluger, Mon 26 Dec 2022 10:44:49 PM UTC
And I still haven't forgot about finishing Term Algebras. I'll need Jean Pierre Serre's "Trees" for that. Am still learning it.
posted by deluger, Fri 23 Dec 2022 06:40:21 AM UTC
Having given up on financial "day jobs" with C and Boolean Algebras (Atomizer), for the past many months or so, I've been working on my new long-term goal in Coq that will take many many years to get to -- exhibiting the free generators of the interval algebra on rational endpoints. I had always wanted to get Topology back into the [...]
posted by deluger, Mon 30 May 2022 04:07:09 PM UTC
My final consensus of Coq is that it's the most powerful language whose behavior no one can explain. People often criticize math formalization for not doing enough. I am officially stopping Coq development after 8 years because it does TOO MUCH. It was the main work that flipped a bit in the Great Spirit and made me happy with honey! Now [...]
posted by deluger, Tue 15 Mar 2022 04:24:35 AM UTC
I always knew Coq wouldn't be enough for my work, both financially and scientifically, and thought that maybe embedded development could complement it, but now I'm putting the embers on low for that. Now aged 45, I gotta think more practically, and nothing's more practical than binary files, and therefore binary file formats, and [...]
posted by deluger, Mon 24 May 2021 03:27:02 AM UTC
The exciting thing in developing a suitable finite type library is realizing that one suitable change to a specific finite type solution carries big consequences as you can develop intricate web-works of inductive types and predicates that relay between [Prop] and [Set] in such a way that keeps the big parameters out of the way. The only way to [...]
posted by deluger, Fri 23 Apr 2021 01:43:11 AM UTC
For the foreseeable future (10+ years) the focus of bool2 will be a clean small group theory interface for embedded solutions. No bigger than small extensions of S4. Canticle is the name of the project that will apply and grow the group theory, and it's part of the bool2 source tree. The goal of Canticle, the device, is to provide bytewise [...]
posted by deluger, Mon 15 Feb 2021 09:56:27 PM UTC
Anyone curious about the alchemical nature of formalization, our real reward, knowing we're putting digital spaces at ease, might be amused by my tarball-size arithmetic that led to 1280000 = 768000 + 512000. 768000 = 512000 + 256000. 512000 = 256000 + 256000. Those 4 numbers appeared as tar-ball sizes, in some Hermetic arithmetic of improvised [...]
posted by deluger, Fri 11 Dec 2020 09:08:54 PM UTC
Partial algebras will still be the math focal point of this
project, because it's ready to go, but there's lots of more important general algebraic math that has to be done on pencil and paper for society's sake, as I hope that financial alchemists will donate a couple thou anonymously to my checking to cover a new computer, as my online laptop
[...]
posted by deluger, Thu 20 Feb 2020 03:27:48 AM UTC
As you can see on the main page, the emphasis in bool2 now will be partial algebras, despite the name, because "bool too" implies the presence of some other main focus, and now the secret is out! I feel lucky to get to have 40 years at a monograph, and still not bet on me finishing it! It's one of the most peaceful-feeling monographs [...]
Powered by Savane 3.13-d3ae.
Corresponding source code