amavect
│u│v│x│y
├─┴─├─┴─
│f │g
├───┴─
│h
└─
│uh│v │xizzy│yeez
├──┴─ ├─────┴────
│fooey │gar
├──────┴───
│hello
└─────
(a+b)+c=a+(b+c)=a+b+c
│a│b │b│c
├─┴─ ├─┴─
│+ │c│a│+ │a│b│c
├───┴─├─┴─ ├─┴─┴─
│+ │+ │+
├─────┴─────┴─
│=
└─
(-b±sqrt(b^2-4*a*c))/(2*a)
│b│2│4│a│c
├─┴─├─┴─┴─
│^ │*
├───┴─
│b│-
├─├─
│-│sqrt│2│a
├─┴────├─┴─
│± │*
├──────┴─
│/
└─
Maybe you read sheet music different than how I do, but when I play euphonium or trombone, I translate from note position+features to finger+mouth position without needing to think about the note letter. More like, "I see the note located here with an accidental feature in the context of the clef and key signature therefore I use this finger position and mouth position". I would love to simplify it down to "it's located here therefore I use this finger position and mouth position".
Keep the accidentals to notate alternate finger positions for enharmonics (and microtones), but eliminate the global variables, the clefs and key signature. Heck, keep the key signature to reduce the noise of alternate fingering symbols, but PLEASE eliminate the clefs. I would also love to play treble clefs at the same sight-reading speed as bass clefs. Also, staff notation should visually repeat every octave, but it doesn't.
Conservation of E-field flux certainly implies additive-homomorphism (addition of charges equals addition of forces). But that seems a bit ahistorical because Maxwell would develop field theory 70 years after Coloumb. Either way, the axiom you choose requires empirical justification, and I think a home hobbyist could more easily demonstrate by experiment that adding charges will add the forces.
Or, if you meant F(r,1,1) = K/r^2, then yeah, conservation of E-field flux could give you an inverse square law. But again, that requires an experiment to justify the axiom.
F(r,q0,q1)
= F(r,q0*1,q1*1)
= q0*q1*F(r,1,1)
I figured this out by listing a bunch of mathematical properties. I couldn't see how the author jumps from zero-preserving to multiply-charges, and I still don't know how, but we can call it out of scope lol
r : distance between p and q
q0 : charge 0
q1 : charge 1
F : coulomb force function
charge-commutative: F(r,q0,q1) = F(r,q1,q0)
zero-preserving: 0 = F(r,q0,0)
additive-homomorphic: F(r,q0,q1+q2) = F(r,q0,q1)+F(r,q0,q2)
homogenous-degree-1: F(r,q0,n*q1) = n*F(r,q0,q1)
multiplicative-separability: F(r,q0,q1) = K*R(r)*Q(q0,q1)
multiply-charges: F(r,q0,q1) = K*R(r)*(q0*q1)^a
Given F(r,q0,q1) = K*R(r)*(q0*q1)^a, charge-commutative, zero-preserving, additive-homomorphic.
Induction using additive-homomorphic proves homogenous-degree-1. (For example, F(r,q0,2*q1) = F(r,q0,q1+q1) = 2*F(r,q0,q1))
Equational proof follows from homogenous-degree-1:
K*R(r)*(q0*n*q1)^a = n*K*R(r)*(q0*q1)^a
(q0*n*q1)^a = n*(q0*q1)^a
n^a*(q0*q1)^a = n*(q0*q1)^a
n^a = n
n = 0 or a = 1
n≠0, therefore a=1.So, you're right. This shows why we should use formal math, so we can agree on the result yet bicker about the interpretation. Some folks point to Cantor's diagonalization theorem to show that some unnameable things exist, when the theorem doesn't say that at all.
On the other hand, given any real number, I can name it. I'll run out of unique names, since no injective function exists from real numbers to names.
So, some unnamed real numbers will always remain (non-constructively), I can make real numbers that escape a naming scheme (constructively), and no unnameable real numbers exist.
Really, the blurb about "seems impossible to verify this by giving positive instances" contains the tension between constructive math and non-constructive math. Does an unnameable (and undefinable) thing actually exist? If a tree falls in a forest, but no one can hear it, does it make a sound?
I love approval voting the most by pure simplicity and effectiveness. How does score voting work better than STAR? I thought STAR degenerates into score voting when clone candidates run?
I haven't heard much of an argument against proportional voting before. Your article just casts doubt, but doesn't really make a decisive argument against. I actually don't like proportional voting because it reifies parties into the system, but I only support it because I think it can break the party duopoly and step towards better systems. I should rethink that.
https://en.wikipedia.org/wiki/Axiom_of_infinity#Independence
https://en.wikipedia.org/wiki/Constructive_analysis#Anti-cla...
I've come to believe that many related incompatible theories have interpretations between each other. For example, hyperbolic geometry has a Euclidean-like Poincare disk model, and Euclidean space exists locally in a hyperbolic space. Boolean logic contains intuitionistic logic (just add the law of excluded middle), but intuitionistic logic contains Boolean logic through the double negation translation. Similar might happen for finite set theories, infinite set theories, and neutral set theories. The fun includes finding the right translation so that we can all enjoy our different tastes in axioms.
In practice, infinite sets never exist as enumerations of every element, but as ways to generate more elements along with descriptions for which elements to include. Infinite set theories allow for equivocating a finite description with the infinite enumeration. In contrast, programming languages usually make a distinction between data (always finite) and data generation (possibly infinite). I would think that counts as a "disproof" in a way.
int factorial_loop_iterative(int n, int a){
while(n > 0){
a = a * n;
n = n - 1;
}
return a;
}
int factorial_loop_recursive(int n, int a){
if(n > 0){
return factorial_loop_recursive(n - 1, a * n);
}else{
return a;
}
}
int factorial_loop_manual(int n, int a){
tailcall:
if(n > 0){
a = a * n;
n = n - 1;
goto tailcall;
}else{
return a;
}
}
int (*factorial_loop)(int n, int a) = factorial_loop_manual;
int factorial(int n){
return factorial_loop(n, 0);
}
Direct health implications of e-cigarette use: a systematic scoping review with evidence assessment https://pmc.ncbi.nlm.nih.gov/articles/PMC11317248/
"Conclusion: Smokers or former smokers who switch to e-cigarettes may reduce their exposure to carcinogens and lower their risk of developing severe health issues associated with conventional smoking. However, in healthy individuals who have never smoked traditional cigarettes, the use of e-cigarettes introduces several cardiovascular and respiratory adverse effects. These findings suggest that while e-cigarettes can be a strategic harm reduction tool for smokers, they are not a safe option for non-smokers."
E-Cigarette Use, Small Airway Fibrosis, and Constrictive Bronchiolitis https://pmc.ncbi.nlm.nih.gov/articles/PMC10137322/
"CONCLUSIONS: After thorough evaluation for other potential etiologies, vaping was considered to be the most likely common causal etiology for all patients due to the temporal association of symptomatic chronic lung disease with e-cigarette use and partial improvement in symptoms after e-cigarette cessation. In this series, we associate the histopathologic pattern of small airway–centered fibrosis, including constrictive bronchiolitis, with vaping, potentially defining a clinical and pathologic entity associated with e-cigarette use. (Funded in part by the National Institutes of Health.)"
E-cigarettes and Vaping: A Smoking Cessation Method or Another Smoking Innovation? https://pmc.ncbi.nlm.nih.gov/articles/PMC9833272/
"Abstract: [cut] With well-known health risks from traditional smoking, e-cigarettes are viewed as a safe way of smoking, appealing more to youth. Additionally, extensive e-cigarette marketing boosted by the internet and fame has resulted in worries that e-cigarettes can lead to a renormalization of cigarette smoking and can be used as a new method to consume vaporized drugs. Although the concern that e-cigarettes are as harmful as traditional smoking has been raised, youth and most healthcare providers remain relatively unaware. [cut]"
And another thing, when 2 underlined terms nest (say, Sn+0=0 with underlines on Sn+0 and n), hovering should highlight only the more specific term (hovering on n highlights both Sn+0 and n the same color).
Also, please remove the rise-in animation so that switching proofs feels faster and less flashy. The rest of the website design has enough flash.
Enough complaints, pretty cool! I did all 20 exercises. Thanks for sharing.
x86 has SETC/SETNC and SETO/SETNO to pull the carry/overflow bits out of the status register.
u+: ADD then SETNC
u-: CMP then SETNC
s+: ADD then SETNO
s-: CMP then SETNO
#include <stdint.h>
#include <stdckdint.h>
int add_u(unsigned x, unsigned y){
return x <= ~y;
}
int sub_u(unsigned x, unsigned y) {
return x <= y;
}
int add_u2(unsigned x, unsigned y){
return !ckd_add(&x, x, y);
}
int sub_u2(unsigned x, unsigned y) {
return !ckd_sub(&x, x, y);
}
int add_s(int x, int y){
return !ckd_add(&x, x, y);
}
int sub_s(int x, int y) {
return !ckd_sub(&x, x, y);
}
So, despite you clearly showing that carry and overflow have the same calculation cost, I don't know how to represent those predicates in a usual math language with equal symbol length or complexity.
We know that universal Turing machines can emulate other Turing machines. Weirdos like Wolfram believe that a universal Turing machine can emulate reality. In a quick skim of this lecture series, the presenter doesn't talk about that, rather he just calls computation a scientific principal (universal and fundamental in the sense of physical laws, not fundamental in the sense of emulating reality on a computer).
More simply put, unsigned addition needs to check that y+x doesn't overflow, while signed addition needs to check that y+x doesn't overflow and doesn't underflow. So, unsigned arithmetic has a simpler precondition that would win a technical debate on whether to use signed or unsigned arithmetic, but since most programming languages lack theorem proving, signed arithmetic wins on the small integer assumption.
size_t i = size;
while(i-- > 0){
// loop body, possibly break
}
use(i); // i wraps below 0
size_t i = size;
while(i > 0){
i--;
// loop body, possibly break
}
use(i); // i doesn't wrap
The safety conditions for unsigned arithmetic:
Ensure y+x ≤ INT_MAX.
If x ≤ UINT_MAX-y, then x+y evaluates correctly:
∀x∀y(x ≤ UINT_MAX-y → ∃z(z = y+x))
Ensure y-x ≤ INT_MAX.
If x≤y, then y-x evaluates correctly:
∀x∀y(x≤y → ∃z(z = y-x))
Ensure INT_MIN ≤ y+x and y+x ≤ INT_MAX.
To avoid overflow or underflow, first compare x to 0.
In the case x≤0, INT_MIN-x cannot underflow, and y+x cannot overflow. If y compares greater than INT_MIN-x, then y+x evaluates correctly.
In the case 0≤x, then INT_MAX-x cannot overflow, and y+x cannot underflow. And if y compares less than INT_MAX-x, then y+x evaluates correctly.
∀x∀y((x≤0 ∧ INT_MIN-x≤y)∨(0≤x ∧ y≤INT_MAX-x) → ∃z(z = y-x))
Ensure INT_MIN ≤ y-x and y-x ≤ INT_MAX.
To avoid overflow or underflow, first compare x to 0.
In the case 0≤x, INT_MIN+x cannot underflow, and y-x cannot overflow. If y compares greater than INT_MIN+x, then y-x evaluates correctly.
In the case x≤0, INT_MAX+x cannot overflow, and y-x cannot underflow. If y compares less than INT_MAX+x, then y-x evaluates correctly.
∀x∀y((0≤x ∧ INT_MIN-x≤y)∨(x≤0 ∧ y≤INT_MAX+x) → ∃z(z = y-x))