text:
## Stream: general

### Topic: computability

#### Kevin Buzzard (Jun 14 2019 at 17:34):

It's about time I understood what Lean means by computability.

import tactic.interactive

-- lean forces me to write noncomputable
noncomputable def g {X Y : Type} (f : X → Y) (hf : function.bijective f) : Y → X :=
begin
intro y,
have h := hf.2 y,
choose x hx using h,
use x
end

#print g -- it's supposed to be noncomputable but it looks like a computer program to me

-- Here I don't need to write noncomputable
theorem g_property {X Y : Type} (f : X → Y) (hf : function.bijective f) (y : Y) :
f (g f hf y) = y :=
begin
exact classical.some_spec (hf.2 y)
end

#print axioms g_property -- classical.choice
-- I used the axiom of choice but I'm computable anyway.

-- and this is computable
def lem (P : Prop) : P ∨ ¬ P := classical.em P

#print axioms lem -- all the axioms

In the definition of g, I am forced to mark it as noncomputable, but what does that mean? I thought proofs were programs. Is my definition of g not a program? My proof of g_property uses the axiom of choice according to #print axioms -- and yet it's computable anyway (in the sense that I was not asked to mark it as noncomputable). And I was not asked to mark my definition of lem as computable, but that's a definition which apparently uses the axiom of choice too. What is going on? It all still looks totally random to me but I think I might understand things enough to actually begin to see what this noncomputable thing which I'm randomly asked to put in front of definitions and possibly theorems (does that happen?) actually means, if someone tries to explain it to me...

#### Kevin Buzzard (Jun 14 2019 at 17:38):

Lean’s standard library defines an additional axiom, propositional extensionality, and a quotient construction which in turn implies the principle of function extensionality. These extensions are used, for example, to develop theories of sets and finite sets. We will see below that using these theorems can block evaluation in Lean’s kernel, so that closed terms of type ℕ no longer evaluate to numerals. But Lean erases types and propositional information when compiling definitions to bytecode for its virtual machine evaluator, and since these axioms only add new propositions, they are compatible with that computational interpretation. Even computationally inclined users may wish to use the classical law of the excluded middle to reason about computation. This also blocks evaluation in the kernel, but it is compatible with compilation to bytecode.

This is from TPIL and it's one of very few parts of the book which I still do not understand. But I don't understand this paragraph at all. I don't know what bytecode is or the virtual machine. I need to be told something easier first.

#### Kevin Buzzard (Jun 14 2019 at 17:40):

What I do understand is that there are conjectures I know such as Waring's problem, where there is a number which I regard as "well-defined", but for which no mathematician knows an algorithm for working them out. I can see that these aren't "computable". I guess I don't see why the other things are computable.

#### Kevin Buzzard (Jun 14 2019 at 17:41):

https://en.wikipedia.org/wiki/Waring%27s_problem

It's known that $4\leq G(3)\leq 7$.

#### Chris Hughes (Jun 14 2019 at 18:01):

It's okay to use choice to make a Sort u, or a proof. If you use it for anything else it's noncomputable.

#### Reid Barton (Jun 14 2019 at 18:01):

I think the rules are simply
1. Types and propositions and proofs are always computable (because they are not actually represented at all at runtime). That is, anything whose type is Sort u for some u. This also extends to Pi-types ending in Sort u.
2. Axioms are not computable (because they have no definition). Normally I think this only applies to choice because the other standard axioms are propositions.
3. Anything that uses something noncomputable is noncomputable, except that rule 1 always takes priority.

#### Reid Barton (Jun 14 2019 at 18:04):

Maybe I've confused myself and rule 1 is really two separate rules (type erasure and proof irrelevance), not sure.

#### Kevin Buzzard (Jun 15 2019 at 08:13):

Ok so perhaps some examples of things which I might want to define are noncomputable nats and noncomputable functions f : X -> Y. So then my next, and I think my last, question is: what am I losing by having these things marked as noncomputable? Is the only difference that I am basically guaranteed not to be able to prove anything about these noncomputable gadgets using rfl? Is that it? I can just reason about these objects perfectly well using exactly the same sort of reasoning I would use in a maths paper. I would never want to use rfl on these objects anyway because I know they've been defined using some choice function.

With things like the perfectoid project I would work constructively by default, and would just write noncomputable in front of a definition every time Lean told me to. I could instead have just written noncomputable theory at the top of every file. What would I have lost if I'd done that? I am struggling to find any reason at all why I would ever care about computability. Let's say my goal was to define a perfectoid space and then state Scholze's tilting correspondence (this is feasible but would take a fair bit more work), and then let's say my next goal was to prove it (this would take an unfeasibly large amount of work unless I had a big team). Would I ever care about computability ever?

#### Mario Carneiro (Jun 15 2019 at 08:30):

Lean produces code for everything that's not marked noncomputable

#### Mario Carneiro (Jun 15 2019 at 08:30):

you can look at this code, although it's not very intelligible

#### Mario Carneiro (Jun 15 2019 at 08:32):

noncomputable theory has no downsides except that it makes computability less obvious (which itself may not be a downside depending on your POV). It actually means "please infer noncomputable for me"

#### Mario Carneiro (Jun 15 2019 at 08:33):

As I'm sure you've noticed, lean knows perfectly well which definitions are computable and which aren't, and without noncomputable theory it nags you until you put the markings it knows you should put. noncomputable theoryjust says to do this automatically without user interaction

#### Kevin Buzzard (Jun 15 2019 at 08:34):

I just don't get why computability is important to me if I just want to make mathematical objects and state and prove theorems about them.

#### Mario Carneiro (Jun 15 2019 at 08:34):

It's not, unless you are Anrdej Bauer

#### Mario Carneiro (Jun 15 2019 at 08:35):

and we're already long past that point since choice appears as an axiom so early in the development that it's difficult to do without

#### Mario Carneiro (Jun 15 2019 at 08:37):

You can still prove stuff about noncomputable gadgets using rfl, as long as you are doing some definition unfolding and such

#### Mario Carneiro (Jun 15 2019 at 08:38):

you won't be able to do large scale rfl proofs like "compute the class number of this field", but I think you know when to use the word "compute" in this context

#### Mario Carneiro (Jun 15 2019 at 08:39):

I think "noncomputable by default, computable for computations" is a reasonable stance for doing pure maths in lean

#### Kevin Buzzard (Jun 15 2019 at 08:40):

I am not sure I know what "computations" mean. Kenny pointed out to me on Thursday at Xena that mathematicians and computer scientists use the term in two different ways.

#### Kevin Buzzard (Jun 15 2019 at 08:40):

I think we use it incorrectly, and I think that the fact that I've been exposed to decades of incorrect usage of the term has clouded my thinking over the issue.

#### Mario Carneiro (Jun 15 2019 at 08:42):

roughly speaking, if you would open up GAP or a CAS to do it

#### Kenny Lau (Jun 15 2019 at 08:42):

then you need a computable model of say Q-bar

#### Mario Carneiro (Jun 15 2019 at 08:43):

sure, that's what I mean by "computable for computations"

#### Mario Carneiro (Jun 15 2019 at 08:43):

unless you need that, computability does you no favors

#### Kevin Buzzard (Jun 15 2019 at 08:57):

The Curry-Howard correspondence says that "proofs are programs". Is there a program corresponding to the proof of the theorem that a product of non-empty sets is non-empty? What is a program? What language is this program supposed to be in?

#### Chris Hughes (Jun 15 2019 at 08:58):

Yes. It's the program that returns (x,y), when x is the witness to X being nonempty, and y is the witness to Y being nonempty.

#### Kevin Buzzard (Jun 15 2019 at 08:58):

infinite product!

#### Kevin Buzzard (Jun 15 2019 at 08:58):

Then you want to give me a function.

#### Kevin Buzzard (Jun 15 2019 at 08:59):

Is there a program corresponding to the proof of the theorem that the Riemann Hypothesis is either true or false?

#### Chris Hughes (Jun 15 2019 at 08:59):

I was thinking about this the other day

#### Kevin Buzzard (Jun 15 2019 at 09:00):

Or maybe the Continuum Hypothesis would be a better example (something which is known not to be provable or disprovable from the axioms of maths)

#### Chris Hughes (Jun 15 2019 at 09:00):

I think you can do this computably

example {ι : Type*} {α : ι → Type*} [S : ∀ i, setoid (α i)]
(f : ∀ i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance)

#### Kevin Buzzard (Jun 15 2019 at 09:01):

If I have P : Prop and then I have some Lean file which makes hP : P, is that definitely a program?

#### Kevin Buzzard (Jun 15 2019 at 09:01):

Even if somewhere along the way, the construction of the term hP uses something noncomputable?

#### Chris Hughes (Jun 15 2019 at 09:02):

In fact you could define this computably in meta using quot.unquot I think, and you would still have a function (even though you used quot.unquot which isn't a mathematical function

#### Kevin Buzzard (Jun 15 2019 at 09:02):

There is something completely fundamental here which I don't understand. A .lean file looks to me like a program, because I can compile it using Lean on my computer. Does this have anything to do with computability though?

#### Chris Hughes (Jun 15 2019 at 09:02):

And this is basically choice if all the quotients are true.

#### Chris Hughes (Jun 15 2019 at 09:03):

I guess it depends what you mean by computable.

#### Kevin Buzzard (Jun 15 2019 at 09:03):

Lean seems to have a perfectly well-defined notion of what it means for something to be computable.

#### Chris Hughes (Jun 15 2019 at 09:04):

.lean files aren't in the domain of that particular computable predicate.

#### Kevin Buzzard (Jun 15 2019 at 09:05):

My understanding is that the initial interpretation of "proof = program" was that a proof was supposed to be interpreted as some sort of proof using only constructive logic or intuitionistic logic or whatever. As we all know, this is not what is going on maths departments across the world -- they have a more powerful notion of proof. Does this just break Curry-Howard, or is there a rigorous but wider interpretation of "program" which I can use which fixes it?

#### Mario Carneiro (Jun 15 2019 at 09:06):

The quotient product example is one place where lean's syntactic notion of "computable" is overly restrictive

#### Kenny Lau (Jun 15 2019 at 09:06):

just use Haskell's setoid-without-quotient philosophy

#### Kenny Lau (Jun 15 2019 at 09:06):

then the quotient.choice is computable

aka setoid hell

#### Kevin Buzzard (Jun 15 2019 at 09:06):

I learnt about that from Nicola Gambini last week.

#### Mario Carneiro (Jun 15 2019 at 09:07):

There are curry howard interpretations of LEM but they are a bit weird

#### Kevin Buzzard (Jun 15 2019 at 09:07):

So Curry-Howard is a lie?

#### Mario Carneiro (Jun 15 2019 at 09:08):

Constructive proofs are programs

#### Chris Hughes (Jun 15 2019 at 09:08):

What I don't quite get is if I have computable choice and computable univalence, shouldn't I be able to get computable em. Obviously I can't, but I don't see where the proof breaks down.

#### Kevin Buzzard (Jun 15 2019 at 09:09):

C-H is pithy, alliterative, beautiful-looking, but not actually true in maths departments because we have a different definition of proof and there is no corresponding definition of program.

#### Mario Carneiro (Jun 15 2019 at 09:09):

I have heard it argued that for most of history mathematics was constructive

#### Kevin Buzzard (Jun 15 2019 at 09:10):

I don't live in the past.

#### Mario Carneiro (Jun 15 2019 at 09:10):

it wasn't until dedekind and such that we started getting a more general notion of function that doesn't readily admit "execution"

#### Mario Carneiro (Jun 15 2019 at 09:11):

You don't need to convince me that you don't see the point in constructivity

#### Kevin Buzzard (Jun 15 2019 at 09:11):

Maybe we can say that the age of Curry-Howard is passed. What I am confused about is the fact that I can prove Tychonoff's theorem (or some other theorem equivalence to the mathematician's axiom of choice) in Lean and make a text file called tykonov.lean which looks to a mathematician like a computer program.

#### Kevin Buzzard (Jun 15 2019 at 09:12):

Is it not a computer program?

It is not

#### Kevin Buzzard (Jun 15 2019 at 09:12):

But I can compile it and it runs.

#### Kevin Buzzard (Jun 15 2019 at 09:12):

It produces no output.

#### Mario Carneiro (Jun 15 2019 at 09:12):

it is input to a computer program that analyzes the information in the file

#### Mario Carneiro (Jun 15 2019 at 09:13):

There are many computer programs in the world, not all of them are compilers

#### Kevin Buzzard (Jun 15 2019 at 09:13):

Aah, so Lean is the program, but my .lean file is not a program?

#### Kevin Buzzard (Jun 15 2019 at 09:13):

I thought Lean compiled my .lean file into an .olean file

#### Mario Carneiro (Jun 15 2019 at 09:13):

Just like when you write TeX code it's input to a program but it's not a program itself, it's just a data representation

#### Mario Carneiro (Jun 15 2019 at 09:14):

unless you write esoteric TeX macros which would be analogous to lean metaprograms which are actually programs

#### Mario Carneiro (Jun 15 2019 at 09:15):

But the key point is this: when you write a proof that is computable in lean, it is literally both a proof and a program

#### Mario Carneiro (Jun 15 2019 at 09:15):

you can run it with #eval

#### Mario Carneiro (Jun 15 2019 at 09:16):

and that's the main idea behind the computability interpretation of intuitionistic math

#### Kevin Buzzard (Jun 15 2019 at 09:16):

macros: I did this in my thesis, which was written in plain TeX (which has no theorem numbering macros); I wrote the macros myself. I think my confusion is now resolved. I don't want to lose track of Chris' question above about computable em, I know he's been thinking a lot about univalence recently. @Gabriel Ebner do you know anything about

What I don't quite get is if I have computable choice and computable univalence, shouldn't I be able to get computable em. Obviously I can't, but I don't see where the proof breaks down.

Mario -- thanks as ever.

#### Kevin Buzzard (Jun 15 2019 at 09:17):

Wait -- I thought the whole problem with HoTT was that univalence wasn't computable? And I have this vague idea that cubical type theory was an attempt to fix this.

that's right

#### Kevin Buzzard (Jun 15 2019 at 09:18):

So Chris it seems to me that you have to become an expert in cubical type theory now.

#### Mario Carneiro (Jun 15 2019 at 09:19):

univalence is not a nonconstructive principle, meaning that we have long believed that it has a constructive interpretation, but as defined in book HoTT it's an axiom, meaning that when you have to "call" it like a function you don't know what to do

#### Mario Carneiro (Jun 15 2019 at 09:20):

In cubical type theory it's a theorem, so the implementation of that function (in terms of new primitives not in HoTT) is now known

#### Mario Carneiro (Jun 15 2019 at 09:20):

Re: univalence and choice, I would try going through DIaconescu with a constructive mindset to see what happens

#### Kevin Buzzard (Jun 15 2019 at 09:21):

I have this uncomfortable feeling about this (univalence axiom). When I was moaning about having built a bunch of structure on a ring R and then wanting to move it onto an isomorphic ring S, people were saying "use HoTT". Now I wonder whether some of the terms I'd get out of this HoTT strategy would just be useless in practice because they have been created using an axiom. On the other hand I guess I make terms using the axiom of choice and seem to get away with it.

#### Mario Carneiro (Jun 15 2019 at 09:22):

It is an open question whether all the consequences of univalence computability are provable in book HoTT. AFAIK it's true

#### Mario Carneiro (Jun 15 2019 at 09:23):

So you wouldn't actually get stuck, but you would need to prove lemmas about how transport works on different structures

#### Mario Carneiro (Jun 15 2019 at 09:23):

(transport is the function a = b -> P a -> P b)

#### Kevin Buzzard (Jun 15 2019 at 09:30):

But the key point is this: when you write a proof that is computable in lean, it is literally both a proof and a program

def X : 2 + 2 = 4 := rfl

#eval X -- #0

#### Kevin Buzzard (Jun 15 2019 at 09:41):

Wait, I am confused again. I thought every proof was computable in Lean, in the sense that you don't have to mark it noncomputable because it's a proof?

#### Alex J. Best (Jun 15 2019 at 09:41):

But the key point is this: when you write a proof that is computable in lean, it is literally both a proof and a program

I'm still amazed by how fast

import data.zmod.quadratic_reciprocity
#eval (zmodp.legendre_sym 1111 3119 (by sorry))

runs.

#### Mario Carneiro (Jun 15 2019 at 09:44):

The caveat is that lean doesn't run what we normally call proofs, i.e. elements of elements of Prop. These are erased in the VM, so they are trivially computable

#### Mario Carneiro (Jun 15 2019 at 09:45):

It is possible to build a theorem prover such that these proofs are executable, and actually lean will reduce proofs if you use #reduce, but there are some efficiency problems with doing this at large scale

#### Kevin Buzzard (Jun 15 2019 at 09:50):

What about my proof that the noncomputable inverse of a bijection was indeed an inverse?

#### Mario Carneiro (Jun 15 2019 at 10:14):

That's computable to a function if you didn't use any axioms

#### Mario Carneiro (Jun 15 2019 at 10:15):

Here's Diaconescu's proof reinterpreted with everything in Type:

open classical
variables (p : Type) {α : Type*} {β : Type*}

inductive eq' (a : α) : α → Type
| refl : eq' a
infix  =' :50 := eq'

def eq'.symm : ∀ {a b : α}, a =' b → b =' a
| _ _ (eq'.refl _) := (eq'.refl _)

def eq'.trans : ∀ {a b c : α}, a =' b → b =' c → a =' c
| _ _ _ (eq'.refl _) (eq'.refl _) := (eq'.refl _)

def eq'.congr_arg (f : α → β): ∀ {a b : α}, a =' b → f a =' f b
| _ _ (eq'.refl a) := eq'.refl _

def eq'.cast : ∀ {a b : Type}, a =' b → a → b
| _ _ (eq'.refl a) := id

def U (x : Type) : Type := x =' unit ⊕ p
def V (x : Type) : Type := x =' empty ⊕ p

def exU : Σ x, U p x := ⟨unit, sum.inl (eq'.refl _)⟩
def exV : Σ x, V p x := ⟨empty, sum.inl (eq'.refl _)⟩

def u : Type := (exU p).fst
def v : Type := (exV p).fst

def u_def : U p (u p) := (exU _).snd
def v_def : V p (v p) := (exV _).snd

def not_uv_or_p : (u p =' v p → empty) ⊕ p :=
begin
cases u_def p with hu hu,
{ cases v_def p with hv hv,
{ refine sum.inl (λ e, _),
exact (hu.symm.trans (e.trans hv)).cast () },
{ exact sum.inr hv } },
{ exact sum.inr hu }
end

axiom funext' {β : α → Type*}
{f₁ f₂ : Π x : α, β x} (h : ∀ x, f₁ x =' f₂ x) : f₁ =' f₂

noncomputable def p_implies_uv (hp : p) : u p =' v p :=
begin
have : U p =' V p,
{ refine funext' (λ x, _),
refine eq'.congr_arg (λ a, a ⊕ p) _,
sorry /- provable by univalence, I'll ignore this -/ },
suffices : ∀ (exU : Σ x, U p x) (exV : Σ x, V p x),
exU.fst =' exV.fst,
{ apply this },
refine @eq'.rec_on _ (U p) (λ W _,
∀ (exU : Σ x, U p x) (exV : Σ x, W x),
exU.fst =' exV.fst) (V p) this _,
assume (exU exV : Σ (x : Type), U p x),
show exU.fst =' exV.fst,
sorry -- We can't prove this. In the original proof
-- exU and exV were proofs and we used proof irrel here,
-- but now it's definitely false; if we reduce everything
-- else (and don't revert exU and exV) we find that
-- exU.fst is unit and exV.fst is empty, so this is false.
end

noncomputable def em : p ⊕ (p → empty) :=
sum.cases_on (not_uv_or_p p)
(λ h, sum.inr (λ e, h (p_implies_uv p e)))
sum.inl

#### Kevin Buzzard (Jun 15 2019 at 12:22):

So this discussion has revealed the fact that I don't really know what a "program" is. I want to define a program as a "computer file" (a lean file, an olean file, a range of memory addresses) which can be turned by a compiler into something which can be run by my CPU. Is that a reasonable definition? Is that Curry-Howard's definition?

I am also a bit confused about definitions. Are definitions also sometimes programs?

Here are two theorems and two definitions.

def D1 : ℕ := 2

theorem T1 : (2 : ℕ) + 2 = 4 := rfl

noncomputable def D2 {X Y : Type} {f : X → Y} (hf : function.surjective f) : Y → X :=
λ y, classical.some (hf y)

theorem T2 (X Y : Type) (f : X → Y) (hf : function.surjective f) (y : Y) : f (D2 hf y) = y :=
classical.some_spec (hf y)

Which of those things can be turned into "programs" in the sense of Curry and Howard?

#### Chris Hughes (Jun 15 2019 at 12:34):

I think I proved trunc (p ⊕ (p → empty)). This is good enough for decidability of all props? Is there any stuff here that doesn't work in HoTT?

import data.quot
open classical
variables (p : Type) {α : Type*} {β : Type*}

inductive eq' (a : α) : α → Type
| refl : eq' a
infix  =' :50 := eq'

def eq'.symm : ∀ {a b : α}, a =' b → b =' a
| _ _ (eq'.refl _) := (eq'.refl _)

def eq'.trans : ∀ {a b c : α}, a =' b → b =' c → a =' c
| _ _ _ (eq'.refl _) (eq'.refl _) := (eq'.refl _)

def eq'.congr_arg (f : α → β): ∀ {a b : α}, a =' b → f a =' f b
| _ _ (eq'.refl a) := eq'.refl _

def eq'.cast : ∀ {a b : Type}, a =' b → a → b
| _ _ (eq'.refl a) := id

def U (x : Type) : Type := x =' unit ⊕ p
def V (x : Type) : Type := x =' empty ⊕ p

def exU : trunc (Σ x : Type, U p x) := trunc.mk ⟨unit, sum.inl (eq'.refl _)⟩
def exV : trunc (Σ x : Type, V p x) := trunc.mk ⟨empty, sum.inl (eq'.refl _)⟩

axiom choice' {ι : Type*} {α : ι → Type*} (f : ∀ i, trunc (α i)) : trunc (Π i, α i)

def not_uv_or_p : ∀ (u : Σ x : Type, U p x) (v : Σ x : Type, V p x), (trunc u.fst =' trunc v.fst → empty) ⊕ p :=
assume u v,
begin
cases u.2 with hu hu,
{ cases v.2 with hv hv,
{ refine sum.inl (λ e, _),
have : trunc unit =' trunc empty, from eq'.rec_on hu (eq'.rec_on hv e),
have : trunc empty, from this.cast (trunc.mk ()),
refine trunc.lift_on this id (assume a, by cases a) },
{ exact sum.inr hv } },
{ exact sum.inr hu }
end

axiom funext' {β : α → Type*}
{f₁ f₂ : Π x : α, β x} (h : ∀ x, f₁ x =' f₂ x) : f₁ =' f₂

noncomputable def p_implies_uv (hp : p) (u : Σ x : Type, U p x) (v : Σ x : Type, V p x) : trunc u.fst =' trunc v.fst :=
begin
have : U p =' V p,
{ refine funext' (λ x, _),
refine eq'.congr_arg (λ a, a ⊕ p) _,
sorry /- provable by univalence, I'll ignore this -/ },
revert u v,
refine eq'.rec_on this _,
assume u v,
sorry, /- Should be provable by univalence. Both types are inhabited -/
end

noncomputable def em : trunc (p ⊕ (p → empty)) :=
have fU : trunc (Π p : Type, Σ x : Type, U p x), from choice' exU,
have fV : trunc (Π p : Type, Σ x : Type, V p x), from choice' exV,
trunc.rec_on_subsingleton fU (assume fU, trunc.rec_on_subsingleton fV (assume fV,
trunc.mk begin
refine sum.rec_on (not_uv_or_p p(fU p) (fV p)) _ _,
{ assume h,
exact sum.inr (assume hp : p, h (p_implies_uv p hp _ _)) },
{ exact sum.inl }
end))

#### Mario Carneiro (Jun 15 2019 at 12:37):

choice' is the actual axiom of choice

#### Chris Hughes (Jun 15 2019 at 12:40):

What's the weaker computable version?

#### Mario Carneiro (Jun 15 2019 at 12:40):

no trunc

it's trivial

#### Mario Carneiro (Jun 15 2019 at 12:41):

People call it the axiom of choice sometimes but it's just moving sigmas around

#### Mario Carneiro (Jun 15 2019 at 12:41):

The thing which is more like the real AC, which is equivalent in power to AC, puts a trunc on each side like you did

#### Chris Hughes (Jun 15 2019 at 12:42):

Without trunc it's the identity function. what do you mean exactly?

#### Mario Carneiro (Jun 15 2019 at 12:43):

Usually people state it as in \forall x, \exists y, p x y -> \exists f, \forall x, p x (f x)

#### Mario Carneiro (Jun 15 2019 at 12:43):

in your form it's particularly simple

#### Mario Carneiro (Jun 15 2019 at 12:44):

So this discussion has revealed the fact that I don't really know what a "program" is. I want to define a program as a "computer file" (a lean file, an olean file, a range of memory addresses) which can be turned by a compiler into something which can be run by my CPU. Is that a reasonable definition? Is that Curry-Howard's definition?

Yes, that's a reasonable definition. The church turing thesis says that basically any reasonable definition of "program" lands on the exact same class of functions, which are the computable functions. A more traditional definition would use turing machines or reduction of lambda terms

#### Chris Hughes (Jun 15 2019 at 12:46):

But my version is still computable

meta def choice2 {ι : Type*} {α : ι → Type*} (f : ∀ i, trunc (α i)) : trunc (Π i, α i) :=
trunc.mk (assume i, quot.unquot (f i))

#### Mario Carneiro (Jun 15 2019 at 12:46):

I am also a bit confused about definitions. Are definitions also sometimes programs?

When you write def in lean, it goes through that compiling bit and produces something that can be run by the CPU, i.e. a program

#### Mario Carneiro (Jun 15 2019 at 12:53):

the choice' isn't needed

noncomputable def em : trunc (p ⊕ (p → empty)) :=
trunc.rec_on_subsingleton (exU p) (assume fU,
trunc.rec_on_subsingleton (exV p) (assume fV,
trunc.mk begin
refine sum.rec_on (not_uv_or_p p fU fV) _ _,
{ assume h,
exact sum.inr (assume hp : p, h (p_implies_uv p hp _ _)) },
{ exact sum.inl }
end))

#### Mario Carneiro (Jun 15 2019 at 13:01):

The nice thing about the computability interpretation is that you can just "inline functions" to find out what happens and maybe end up proving something much stronger:

noncomputable def em : (p → empty) :=
begin
let u : Σ x : Type, U p x := ⟨unit, sum.inl (eq'.refl _)⟩,
let v : Σ x : Type, V p x := ⟨empty, sum.inl (eq'.refl _)⟩,
have h : trunc u.fst =' trunc v.fst → empty,
{ intro e,
have : trunc unit =' trunc empty, from e,
have : trunc empty, from this.cast (trunc.mk ()),
refine trunc.lift_on this id (assume a, by cases a) },
exact assume hp : p, h (p_implies_uv p hp _ _),
end

#### Mario Carneiro (Jun 15 2019 at 13:16):

Okay, it's completely self contained now. Clearly something is odd

import data.quot
open classical
variables (p : Type) {α : Type*} {β : Type*}

inductive eq' (a : α) : α → Type
| refl : eq' a
infix  =' :50 := eq'

def eq'.symm : ∀ {a b : α}, a =' b → b =' a
| _ _ (eq'.refl _) := (eq'.refl _)

def eq'.trans : ∀ {a b c : α}, a =' b → b =' c → a =' c
| _ _ _ (eq'.refl _) (eq'.refl _) := (eq'.refl _)

def eq'.congr_arg (f : α → β): ∀ {a b : α}, a =' b → f a =' f b
| _ _ (eq'.refl a) := eq'.refl _

def eq'.cast : ∀ {a b : Type}, a =' b → a → b
| _ _ (eq'.refl a) := id

axiom funext' {β : α → Type*}
{f₁ f₂ : Π x : α, β x} (h : ∀ x, f₁ x =' f₂ x) : f₁ =' f₂

noncomputable def hm : empty :=
let U (x : Type) : Type := x =' unit in
let V (x : Type) : Type := x =' empty in
begin
let u : Σ x : Type, U x := ⟨unit, eq'.refl _⟩,
let v : Σ x : Type, V x := ⟨empty, eq'.refl _⟩,
have : trunc u.fst =' trunc v.fst,
{ have : U =' V,
{ refine funext' (λ x, _),
dsimp [U, V],
sorry /- provable by univalence, I'll ignore this -/ },
generalize : u = u', generalize : v = v',
clear u v, revert u' v',
refine eq'.rec_on this (λ (u v : Σ x, x =' unit), _),
sorry, /- Should be provable by univalence. Both types are inhabited -/
},
have : trunc empty, from this.cast (trunc.mk ()),
exact trunc.lift_on this id (assume a, by cases a)
end

#### Mario Carneiro (Jun 15 2019 at 13:24):

Aha, of course:

example (H : ∀ x, (x =' unit) =' (x =' empty)) : empty :=
((H unit).cast (eq'.refl _)).cast ()

#### Chris Hughes (Jun 15 2019 at 13:25):

So does that mean axiom univalence {α β : Sort*} : α ≃ β → α = β is inconsistent with Lean?

#### Chris Hughes (Jun 15 2019 at 13:25):

because funext' is provable in Lean

#### Mario Carneiro (Jun 15 2019 at 13:25):

the first sorry is false

#### Reid Barton (Jun 15 2019 at 13:25):

I don't understand how you intend to prove x =' unit =' (x =' empty)

Yeah

#### Chris Hughes (Jun 15 2019 at 13:26):

I didn' check that one

#### Kevin Buzzard (Jun 15 2019 at 13:32):

I am also a bit confused about definitions. Are definitions also sometimes programs?

When you write def in lean, it goes through that compiling bit and produces something that can be run by the CPU, i.e. a program

So D1 and T1 (the definition and theorem which worked in vanilla Lean with no classical or anything) are turned into programs by the Lean executable, and D2 is probably not (because it's not computable), and I'm still a bit confused about T2.

#### Kevin Buzzard (Jun 15 2019 at 13:34):

Hey that univalence axiom looks really useful! Maybe someone should ask Leo to add it.

#### Mario Carneiro (Jun 15 2019 at 13:35):

Only D1 actually gets associated bytecode

#### Kevin Buzzard (Jun 15 2019 at 13:35):

I don't know what bytecode is. I want to know which ones become programs, or perhaps can become programs.

#### Mario Carneiro (Jun 15 2019 at 13:35):

that's CS speak for "the thing the computer runs"

#### Kevin Buzzard (Jun 15 2019 at 13:36):

TeX -- you can write a file, but it's not a program. Is bytecode always a program?

#### Mario Carneiro (Jun 15 2019 at 13:37):

bytecode is stuff that gets run by an interpreter. It's the equivalent of compilation for interpreted languages

like python

#### Kevin Buzzard (Jun 15 2019 at 13:37):

@Chris Hughes I can make a term of type equiv nat int. If I can deduce nat = int and I have -1 : int, can I then make -1 : nat?

no

#### Mario Carneiro (Jun 15 2019 at 13:37):

you get cast _ (-1) : nat

#### Kevin Buzzard (Jun 15 2019 at 13:38):

If I make two different equivs from nat to int, deduce nat = int twice, and use both deductions to move from int to nat, can I deduce cast _ (-1) : nat = cast _ (-1) : nat?

#### Kevin Buzzard (Jun 15 2019 at 13:38):

Is the _ a missing proof or missing data?

#### Mario Carneiro (Jun 15 2019 at 13:39):

missing proof, but proofs are data in HoTT

#### Mario Carneiro (Jun 15 2019 at 13:39):

in lean the proofs are defeq and so you would get in trouble at this point

#### Kevin Buzzard (Jun 15 2019 at 13:39):

So does that mean axiom univalence {α β : Sort*} : α ≃ β → α = β is inconsistent with Lean?

This was the question I was interested in. Is it inconsistent?

no

#### Mario Carneiro (Jun 15 2019 at 13:40):

That's actually weak univalence; I think it's consistent

#### Kevin Buzzard (Jun 15 2019 at 13:42):

bytecode is stuff that gets run by an interpreter. It's the equivalent of compilation for interpreted languages

So the bytecode made with D1 is a program. And there's no bytecode made for T1 but if we weren't so proof-impredicative then there could be a program made for T1. And there's no program for D2, and there's no program for T2 but that's for two reasons -- firstly because the VM forgets all proofs, and secondly because even if it didn't, it wouldn't be able to make the program because there's no program for D2. Have I finally got this straight?

#### Kevin Buzzard (Jun 15 2019 at 13:43):

In HoTT there could be a program for T1 but not for T2

#### Mario Carneiro (Jun 15 2019 at 13:43):

Yes. More precisely, it could try to make programs for D2 and T2, but somewhere in there there would be a call to the function choice()

#### Mario Carneiro (Jun 15 2019 at 13:43):

and that function has no definition

#### Mario Carneiro (Jun 15 2019 at 13:43):

like we have no clue how to write a function that works

#### Kevin Buzzard (Jun 15 2019 at 13:43):

nat.zero has no definition.

#### Mario Carneiro (Jun 15 2019 at 13:43):

it is defined to return 0

in the bytecode

#### Mario Carneiro (Jun 15 2019 at 13:44):

we know how to implement inductive types, by using tagged unions

#### Kevin Buzzard (Jun 15 2019 at 13:44):

I think I would like to see some simple examples of what bytecode looks like. How do I do this? I've inspected it in the past with a text editor and that didn't end well.

#### Mario Carneiro (Jun 15 2019 at 13:45):

set_option trace.compiler.optimize_bytecode true

#### Mario Carneiro (Jun 15 2019 at 13:45):

don't ask why the name of the option is so not obvious

#### Kevin Buzzard (Jun 15 2019 at 13:46):

def D1 : ℕ := 2
/-
[compiler.optimize_bytecode]  D1 0
0: scnstr #2
1: ret
-/

and is there somewhere which gives me some idea of what these commands like scnstr mean?

#### Mario Carneiro (Jun 15 2019 at 13:48):

no, you have to guess but I can take a stab

#### Mario Carneiro (Jun 15 2019 at 13:49):

I think it is "simple constructor #2" which builds a simple atom (a nat) with value 2

ret is return

#### Kevin Buzzard (Jun 15 2019 at 13:52):

I'm stuck on this one:

set_option trace.compiler.optimize_bytecode true

inductive A
| a : A
| b : A

open A

def D : list A := [a, b, a]
/-
[compiler.optimize_bytecode]  D 0
0: scnstr #0
1: scnstr #1
2: scnstr #0
3: scnstr #0
4: cnstr #1 2
5: cnstr #1 2
6: cnstr #1 2
7: ret
-/

#### Kevin Buzzard (Jun 15 2019 at 13:52):

Hey, wait a minute! This code has line numbers! It's like BBC Basic! It's like the old days! Hey this is a program, right?

#### Mario Carneiro (Jun 15 2019 at 13:57):

this is a very low level program indeed

#### Mario Carneiro (Jun 15 2019 at 13:58):

and it has line numbers because there is a goto

#### Kevin Buzzard (Jun 15 2019 at 14:01):

\me remembers the old days

#### Kevin Buzzard (Jun 15 2019 at 14:01):

darn it, I'm sure some variant of that works

#### Kenny Lau (Jun 15 2019 at 14:02):

set_option trace.compiler.optimize_bytecode true

inductive A
| a : A
| b : A

open A

def D1 : list A := []
/-
[compiler.optimize_bytecode]  D1 0
0: scnstr #0
1: ret
-/

def D2 : list A := [a]
/-
[compiler.optimize_bytecode]  D2 0
0: scnstr #0
1: scnstr #0
2: cnstr #1 2
3: ret
-/

def D3 : list A := [b, a]
/-
[compiler.optimize_bytecode]  D3 0
0: scnstr #1
1: scnstr #0
2: scnstr #0
3: cnstr #1 2
4: cnstr #1 2
5: ret
-/

def D4 : list A := [a, b, a]
/-
[compiler.optimize_bytecode]  D4 0
0: scnstr #0
1: scnstr #1
2: scnstr #0
3: scnstr #0
4: cnstr #1 2
5: cnstr #1 2
6: cnstr #1 2
7: ret
-/

#### Kevin Buzzard (Jun 15 2019 at 14:03):

That makes it much clearer.

#### Kevin Buzzard (Jun 15 2019 at 14:03):

oh wait actually it does make it clearer.

#### Kevin Buzzard (Jun 15 2019 at 14:04):

def D : list A := [b, b, a]
/-
[compiler.optimize_bytecode]  D 0
0: scnstr #1
1: scnstr #1
2: scnstr #0
3: scnstr #0
4: cnstr #1 2
5: cnstr #1 2
6: cnstr #1 2
7: ret
-/

The code is backwards or something.

#### Mario Carneiro (Jun 15 2019 at 14:04):

It works like a stack machine. Here's what the stack looks like, pushing items from the right:

   []
0: [#0]
1: [#0, #1]
2: [#0, #1, #0]
3: [#0, #1, #0, #0]
4: [#0, #1, #1 #0 #0]
5: [#0, #1 #1 (#1 #0 #0)]
6: [#1 #0 (#1 #1 (#1 #0 #0))]

the final line returns the value on the stack, which is #1 #0 (#1 #1 (#1 #0 #0))

#### Mario Carneiro (Jun 15 2019 at 14:05):

if you squint, you can read #0 and #1 as the constructors of both list and A, and see cons a (cons b (cons a nil))

#### Kevin Buzzard (Jun 15 2019 at 14:05):

aah of course I'd forgotten about list.nil

#### Kevin Buzzard (Jun 15 2019 at 14:09):

So cons and list and stuff are all being turned into bytecode. And the point is that choice cannot be turned into bytecode. So here is a proof

noncomputable def g {X Y : Type} {f : X → Y} (hf : function.surjective f) (y : Y) : X := classical.some (hf y)

def g_prop {X Y : Type} {f : X → Y} (hf : function.surjective f) (y : Y) := classical.some_spec (hf y)

theorem has_right_inverse_of_surjective (X Y : Type) (f : X → Y) (hf : function.surjective f) :
∃ g : Y → X, ∀ y : Y, f (g y) = y := ⟨g hf, g_prop hf⟩

which cannot be made into a program and which is hence a counterexample to a completely naive interpretation of the Curry-Howard correspondence that "proofs equal programs".

#### Kenny Lau (Jun 15 2019 at 14:12):

set_option trace.compiler.optimize_bytecode true

inductive A : Type | a | b (c : A)

def E : A := A.b (A.b A.a)
def F : ℕ := nat.succ (nat.succ nat.zero)
def G : ℕ := 2

/-
sandbox3.lean:5:0: information trace output
[compiler.optimize_bytecode]  E 0
0: scnstr #0
1: cnstr #1 1
2: cnstr #1 1
3: ret

sandbox3.lean:6:0: information trace output
[compiler.optimize_bytecode]  F 0
0: scnstr #1
1: cfun nat.succ
2: ret

sandbox3.lean:7:0: information trace output
[compiler.optimize_bytecode]  G 0
0: scnstr #2
1: ret
-/

#### Kenny Lau (Jun 15 2019 at 14:12):

why are F and G different?

#### Mario Carneiro (Jun 15 2019 at 14:13):

for some reason nat.succ was not optimized away in F

#### Kenny Lau (Jun 15 2019 at 14:13):

why are all of them different?

#### Mario Carneiro (Jun 15 2019 at 14:14):

Obviously the VM does not represent natural numbers as unary, so succ (succ zero) and 2 are not the same thing

#### Mario Carneiro (Jun 15 2019 at 14:14):

2 is stored as a 2 in memory

#### Kevin Buzzard (Jun 15 2019 at 14:14):

This trace.compiler.optimize_bytecode should win set_option option of the week.

lol

#### Johan Commelin (Jun 15 2019 at 14:15):

\me remembers the old days

In the old days it was /me...

#### Mario Carneiro (Jun 15 2019 at 14:15):

/me thinks it still is

#### Kenny Lau (Jun 15 2019 at 14:15):

why is E and F different at all?

#### Kevin Buzzard (Jun 15 2019 at 14:16):

def N := 100000000
/-
[compiler.optimize_bytecode]  N 0
0: scnstr #100000000
1: ret
-/
def M := 10000000000
/-
[compiler.optimize_bytecode]  M 0
0: num 10000000000
1: ret
-/

#### Mario Carneiro (Jun 15 2019 at 14:16):

num is for really big numbers that don't fit in the size of a small nat

#### Mario Carneiro (Jun 15 2019 at 14:16):

which is something like 2^30

#### Johan Commelin (Jun 15 2019 at 14:16):

/me thinks @Mario Carneiro is from the old days...

#### Mario Carneiro (Jun 15 2019 at 14:17):

/me doesn't know how to use status messages properly

#### Johan Commelin (Jun 15 2019 at 14:18):

In the old days one used .plan

#### Kevin Buzzard (Jun 15 2019 at 14:18):

#help options

So much still to learn!

#### Kevin Buzzard (Jun 15 2019 at 14:18):

I remember disabling finger by creating a pipe called .plan somehow.

#### Kevin Buzzard (Jun 15 2019 at 14:19):

In the old days you could see if your friend had read your email to them by just fingering them.

#### Mario Carneiro (Jun 15 2019 at 14:19):

@Kenny Lau E and F are different because lean has special support for the nat inductive type

#### Kevin Buzzard (Jun 15 2019 at 14:20):

Can we see the state of the stack machine easily?

#### Mario Carneiro (Jun 15 2019 at 14:20):

One of the ideas in 3.5c is to make such overrides more obvious

#### Kevin Buzzard (Jun 15 2019 at 14:20):

[I mean, in the middle of some calculation]

#### Mario Carneiro (Jun 15 2019 at 14:21):

I think there is a debugger but I've never used it

#### Mario Carneiro (Jun 15 2019 at 14:21):

it's written in lean

#### Kevin Buzzard (Jun 15 2019 at 14:21):

I thought you wrote some code which somehow "read" olean files? Oh -- olean files are yet another thing somehow?

#### Kevin Buzzard (Jun 15 2019 at 14:21):

We're looking at the bytecode expressed in a far more sane way.

#### Mario Carneiro (Jun 15 2019 at 14:22):

this is all actually somewhat unrelated to olean files

#### Mario Carneiro (Jun 15 2019 at 14:23):

olean files are basically a compressed representation of everything that goes in a lean file and all the stuff that is generated as a result of running it

#### Mario Carneiro (Jun 15 2019 at 14:23):

the idea is that you can read an olean file and it will be just as good as reading the lean file but without having to run all the tactics

#### Olli (Jun 15 2019 at 14:24):

Wikipedia says that Lambda-mu calculus has classical proofs as programs, where AoC and double-negation elimination map to continuations

#### Mario Carneiro (Jun 15 2019 at 14:24):

right, that's the "a bit weird" part I mentioned. Double negation elimination has a computational implementation

#### Olli (Jun 15 2019 at 14:33):

I know continuations are useful for implementing control flow / concurrency, so I suppose if a constructive proof describes an algorithm, then a classical proof is one that contains a step that says "yes, let me get back to you on that", in which case you could think of sorry as a type of continuation

#### Mario Carneiro (Jun 15 2019 at 14:42):

I like to think of call/cc for LEM via oracles and time travel. You ask the oracle "Is RH true?" and it says NO, and gives you a token that says RH -> false. You celebrate the resolution of the long standing problem, until one day when someone finds that RH is actually true. But when you confront the oracle with your proof of falsity, it takes your proof of RH, destroys the universe and rewinds to the original question, and when asked "Is RH true?" it says YES and gives you a bloodstained proof of RH, and you celebrate the resolution of the long standing problem.

#### Kevin Buzzard (Jun 15 2019 at 15:30):

What about choice()?

#### Kevin Buzzard (Jun 15 2019 at 17:27):

https://xenaproject.wordpress.com/2019/06/15/proofs-are-not-programs/

Hopefully I haven't garbled too much of this conversation.

#### Johan Commelin (Jun 15 2019 at 19:06):

@Kevin Buzzard I think this is possible because of computable code:

@[simp] lemma witt_add_zero : witt_add p 0 = X (tt, 0) + X (ff, 0) :=
dec_trivial

@[simp] lemma witt_mul_zero : witt_mul p 0 = X (tt, 0) * X (ff, 0) :=
dec_trivial

#### Johan Commelin (Jun 15 2019 at 19:06):

Lean is computing the addition and multiplication on the zeroth truncation of Witt vectors

Would rfl work?

Let me try.

#### Johan Commelin (Jun 15 2019 at 19:12):

type mismatch, term
rfl
has type
?m_2 = ?m_2
but is expected to have type
witt_add p 0 = X (tt, 0) + X (ff, 0)

Nope (-;

#### Johan Commelin (Jun 15 2019 at 19:13):

And that's not surprising. Because it isn't even close to being the definition of witt_add.

#### Johan Commelin (Jun 15 2019 at 19:14):

@Mario Carneiro This is one reason (quite small, I agree) to keep polynomials computable.

#### Chris Hughes (Jul 13 2019 at 21:09):

I answered my own question about computable choice. The definition I suggested for computable choice is very much inconsistent. The definition was

meta def choice {α : Sort*} {β : α → Sort*} : (Π a, trunc (β a)) → trunc (Π a, β a) :=
λ f, trunc.mk (λ a, quot.unquot (f a))

I claimed that this was a function, but it isn't. Using choice on (id : trunc bool -> trunc bool) gives nonsense

import data.quot logic.basic

meta def choice {α : Sort*} {β : α → Sort*} : (Π a, trunc (β a)) → trunc (Π a, β a) :=
λ f, trunc.mk (λ a, quot.unquot (f a))

def decidable_true (choice : Π {α : Sort*} {β : α → Sort*}
(f : Π a, trunc (β a)), trunc (Π a, β a)) : decidable true :=
trunc.rec_on_subsingleton (choice (id : trunc bool → trunc bool))
(λ f, decidable_of_iff (f (trunc.mk tt) = f (trunc.mk ff))
(by rw [subsingleton.elim (trunc.mk tt) (trunc.mk ff)]; exact eq_self_iff_true _))

#eval decidable_true @choice --ff
`

Last updated: May 15 2021 at 00:39 UTC


text:
Skip to main content

Loading table of contents menu...

# 9.16: Hypothesis Test for Difference in Two Population Proportions (3 of 6)

Learning Objectives

• Under appropriate conditions, conduct a hypothesis test for comparing two population proportions or two treatments. State a conclusion in context.
• Interpret the P-value as a conditional probability.

## Details of This Hypothesis Test

In a hypothesis test, we base our conclusion on the P-value. Where does the P-value come from? The P-value comes from a normal model of the sampling distribution of differences in sample proportions. In “Distribution of Differences in Sample Proportions,” we saw that a normal model is a good fit for the sampling distribution if each sample has at least 10 successes and failures.

We learned that the sampling distribution has the following center and spread.

$\begin{array}{l}\text{}\mathrm{mean}\text{}=\text{}{p}_{1}-{p}_{2}\\ \mathrm{standard}\text{}\mathrm{error}\text{}=\text{}\sqrt{\frac{{p}_{1}(1-{p}_{1})}{{n}_{1}}+\frac{{p}_{2}(1-{p}_{2})}{{n}_{2}}}\end{array}$

In the hypothesis test, we do not make a claim about either population proportion, so we do not have values for p1 and p2. For a confidence interval, we used the sample proportions, ${\stackrel{ˆ}{p}}_{1}$ and ${\stackrel{ˆ}{p}}_{2}$, to estimate those values. Here we use a different estimate. Since the null hypothesis states that the population proportions are equal, we use the same estimate for both population proportions.

To do this, we combine the samples to create a pooled proportion. Here, x1 and x2 are the numbers of successes in the respective samples of sizes n1 and n2. We use the pooled proportion as an estimate for both population proportions.

$\stackrel{ˆ}{p}\text{}=\text{}\frac{{x}_{1}\text{}+\text{}{x}_{2}}{{n}_{1}\text{}+\text{}{n}_{2}}$

In a hypothesis test, we use the pooled proportion to estimate the standard error.

$\begin{array}{l}\\ \mathrm{estimated}\text{}\mathrm{standard}\text{}\mathrm{error}\text{}=\text{}\sqrt{\frac{\stackrel{ˆ}{p}(1-\stackrel{ˆ}{p})}{{n}_{1}}+\frac{\stackrel{ˆ}{p}(1-\stackrel{ˆ}{p})}{{n}_{2}}}\end{array}$

We use the estimated standard error to calculate the Z-test statistic.

$Z\text{}=\text{}\frac{\mathrm{statistic}\text{}-\text{}\mathrm{parameter}}{\mathrm{standard}\text{}\mathrm{error}}$

$Z\text{}=\text{}\frac{(\mathrm{difference}\text{}\mathrm{in}\text{}\mathrm{sample}\text{}\mathrm{proportions})\text{}-\text{}(\mathrm{difference}\text{}\mathrm{in}\text{}\mathrm{population}\text{}\mathrm{proportions})}{\mathrm{standard}\text{}\mathrm{error}}$

$Z\text{}=\text{}\frac{({\stackrel{ˆ}{p}}_{1}-{\stackrel{ˆ}{p}}_{2})\text{}-\text{}({p}_{1}-{p}_{2})}{\sqrt{\frac{\stackrel{ˆ}{p}\text{}(1-\stackrel{ˆ}{p})\text{}}{{n}_{1}}+\frac{\stackrel{ˆ}{p}\text{}(1-\stackrel{ˆ}{p})}{{n}_{2}}}}$

Since p1p2 = 0 in the null hypothesis, the Z-test statistic simplifies to the following:

$Z\text{}=\text{}\frac{({\stackrel{ˆ}{p}}_{1}-{\stackrel{ˆ}{p}}_{2})\text{}-\text{}0}{\sqrt{\frac{\stackrel{ˆ}{p}\text{}(1-\stackrel{ˆ}{p})\text{}}{{n}_{1}}+\frac{\stackrel{ˆ}{p}\text{}(1-\stackrel{ˆ}{p})}{{n}_{2}}}}$

After we calculate the Z-test statistic, we use a simulation or other technology to find the P-value from the standard normal curve.

## Comparing Wal-Mart’s with Other Firms’ Insurance Coverage

Recall the 2003 press release by the AFL-CIO:

• Wal-Mart exemplifies the harmful trend among America’s large employers to shirk health insurance responsibilities at the cost of their workers and community….Fewer than half of Wal-Mart workers are insured under the company plan – just 46 percent. This rate is dramatically lower than the 66 percent of workers at large private firms who are insured under their companies’ plans, according to a new Commonwealth Fund study released today.

This press release claims that there is a 20% difference in the proportion of workers with insurance when we compare Wal-Mart to other large private firms. In hypothesis testing for two population proportions, we cannot test a claim about a specific difference between two population proportions. Instead, we test a claim that the proportion of Wal-Mart workers with health insurance is less than the proportion of workers at large private firms with health insurance.

Suppose we select a random sample of 50 Wal-Mart workers and find 23 have health insurance. Suppose also that a random sample of 70 workers of large private firms had 43 with health insurance.

For this test, we choose a 5% level of significance (α = 0.05).

Step 1: State the hypotheses.

Let p1 and p2 represent the proportions of workers with health insurance among Wal-Mart and large private company employees respectively.

The null hypothesis is a claim of “no difference”: H0: p1p2 = 0. The alternative hypothesis states that the population proportion is lower for Wal-Mart employees: p1 < p2. The difference is less than zero, so it is negative: Ha: p1p2 < 0.

Step 2: Collect the data.

Of 50 Wal-Mart workers, 23 have health insurance. Of 70 workers from large private firms, 33 have health insurance. From the data, we can calculate the difference in sample proportions.

${\stackrel{ˆ}{p}}_{1}-{\stackrel{ˆ}{p}}_{2}=\frac{23}{50}-\frac{43}{70}\approx-0.154$

Step 3: Assess the evidence.

Check the Normality Criteria

Determine if a normal model is a good fit for the sampling distribution. Verify that there are at least 10 successes and failures in each sample. Here, a success is an employee with health insurance. In the Wal-Mart sample, there are 23 successes and 50 − 23 = 27 failures. In the large private firms sample, there are 43 successes and 27 failures. Each of these is at least 10, so we can use the normal model.

Compute the Test Statistic (only if the normal model is a good fit)

The test statistic requires the standard error. To compute the standard error, we first compute the pooled proportion.

$\stackrel{ˆ}{p}\text{}=\text{}\frac{{x}_{1}\text{}+\text{}{x}_{2}}{{n}_{1}\text{}+\text{}{n}_{2}}\text{}=\text{}\frac{23\text{}+\text{}43}{50\text{}+\text{}70}\text{}=\text{}\frac{66}{120}\text{}=\text{}0.55$

We use the pooled proportion to estimate the standard error.

$\sqrt{\frac{\stackrel{ˆ}{p}(1-\stackrel{ˆ}{p})}{{n}_{1}}+\frac{\stackrel{ˆ}{p}(1-\stackrel{ˆ}{p})}{{n}_{2}}}\text{}=\text{}\sqrt{\frac{0.55(0.45)}{50}+\frac{0.55(0.45)}{70}}\text{}\approx \text{}0.092$

Recall the difference in sample proportions from the data.

${\stackrel{ˆ}{p}}_{1}-{\stackrel{ˆ}{p}}_{2}\text{}=\text{}\frac{23}{50}-\frac{43}{70}\text{}\approx \text{}-0.154$

We use the z-score to determine how many standard errors −0.154 is from the mean of 0.

$Z\text{}=\text{}\frac{({\stackrel{ˆ}{p}}_{1}-{\stackrel{ˆ}{p}}_{2})\text{}-\text{}({p}_{1}-{p}_{2})}{\sqrt{\frac{\stackrel{ˆ}{p}\text{}(1-\stackrel{ˆ}{p})\text{}}{{n}_{1}}+\frac{\stackrel{ˆ}{p}\text{}(1-\stackrel{ˆ}{p})}{{n}_{2}}}}\text{}\approx \text{}\frac{-0.154-0}{0.092}\text{}\approx \text{}-1.67$

Note: A z-score of −1.67 tells us that the observed difference of ${\stackrel{ˆ}{p}}_{1}-{\stackrel{ˆ}{p}}_{2}$ = −0.154 is 1.67 standard errors below the assumed difference of zero. Does this suggest that the observed difference is statistically significant? Since we stated a significance level of 5%, we need to find the P-value and compare it to 0.05.

Identify the P-Value

We use a simulation. We want the probability that the difference in sample proportions is less than −0.154. This corresponds to the probability that Z is less than −1.67. So we use the area to the left of the Z-test statistic. The P-value is about 0.047. If you like symbols, we can write this in mathematical notation.

$P\text{}(\text{}({\stackrel{ˆ}{p}}_{1}-{\stackrel{ˆ}{p}}_{2})\text{}<-0.154\text{})\text{}=\text{}P\text{}(Z\text{}<-1.67)\text{}\approx \text{}0.047$

The P-value is small, about 4.7%. It means that if there is no difference in the population proportions, there is about a 4.7% chance that random samples will have a difference less than −0.154. The difference we observed in our samples, then, is fairly unlikely. We do not think this difference is due to chance. We see that the P-value is less than 5%, so we conclude that the difference we observed is statistically significant.

Step 4: State a conclusion.

Use the P-Value to Make a Decision

A P-value less than the significance level means we reject the null hypothesis. So we support the alternative hypothesis, p1p2 < 0, or more simply, p1 < p2. The given sample data support the claim that the proportion of Wal-Mart workers with health insurance is lower than the proportion of workers for large private companies.

## Comment

If a normal model is a good fit for the sampling distribution, we use it to find the P-value. But let’s look at a simulation of the sampling distribution to remind ourselves what the P-value really means.

The simulation can help us understand the P-value. In the simulation, we assume that the population proportions are the same, so the difference is 0. This is the null hypothesis. We assume the null hypothesis is true and select thousands of random samples from populations with the same proportion of successes. The mean of the sampling distribution is 0 (as predicted by the null hypothesis). We see this in the simulated sampling distribution on the left.

We mark the difference in the sample proportions from our data. It is 23/50 − 43/70 = -0.15. This difference has a z-score of −1.67. In the simulation of the sampling distribution, we can see that a difference smaller than −0.15 is unlikely. Very few samples have a difference less than −0.15. The normal model shows that the probability is about 4.7%.

Putting this all together, we have the formal definition of the P-value. The P-value is the probability that random samples have results at least as extreme as the data if the null hypothesis is true. We can also describe the P-value in terms of z-scores. The P-value is the probability that the test statistic has a value more extreme than that associated with the data if the null hypothesis is true.

## Are There Gender Differences in Teen Depression Rates?

Previous studies suggest that female teens are more likely than male teens to be depressed. Define the depression rates for the female and male teens as p1 and p2 respectively. If we claim that the depression rate is higher for female teens (p1 > p2), the null and alternative hypotheses are:

• H0: p1p2 = 0
• Ha: p1p2 > 0

Let’s test the hypotheses at a 5% significance level. Suppose we randomly select 100 female teens and determine that 14 are clinically depressed. Among 200 randomly selected male teens, 16 are clinically depressed.

https://assessments.lumenlearning.co...sessments/3646

Since the normal model is a good fit, we can use the standard normal curve to find the P-value. We used a simulation. The P-value is about 0.051.

https://assessments.lumenlearning.co...sessments/3647

https://assessments.lumenlearning.co...sessments/3660

## Contributors and Attributions

CC licensed content, Shared previously

9.16: Hypothesis Test for Difference in Two Population Proportions (3 of 6) is shared under a not declared license and was authored, remixed, and/or curated by LibreTexts.

• Was this article helpful?

format: plain


text:
# Compositions of Quadratic Forms (De Gruyter Expositions in by Daniel B. Shapiro

By Daniel B. Shapiro

The principal subject of this booklet is the concept of Hurwitz and Radon bearing on composition formulation for sums of squares, first proved within the 1920's. ideas from algebra and topology are used to generalize that theorem in different instructions. The textual content contains labored examples and lots of workouts, which boost nonetheless extra diversifications of the vital subject. the most viewers is those who have had a few graduate classes in summary algebra, yet many sections of the booklet are available to a person with a few education in linear algebra. a number of significant subject matters during this booklet can be of curiosity to scholars of topology and geometry. the writer has tried to make the presen-tation as transparent and as trouble-free as attainable.

Read or Download Compositions of Quadratic Forms (De Gruyter Expositions in Mathematics) PDF

Similar number theory books

Number Theory 1: Fermat's Dream

This is often the English translation of the unique eastern ebook. during this quantity, "Fermat's Dream", middle theories in sleek quantity concept are brought. advancements are given in elliptic curves, $p$-adic numbers, the $\zeta$-function, and the quantity fields. This paintings offers a sublime viewpoint at the ask yourself of numbers.

Initial-Boundary Value Problems and the Navier-Stokes Equations

This ebook offers an creation to the great topic of preliminary and initial-boundary worth difficulties for PDEs, with an emphasis on purposes to parabolic and hyperbolic platforms. The Navier-Stokes equations for compressible and incompressible flows are taken to illustrate to demonstrate the consequences.

Additional info for Compositions of Quadratic Forms (De Gruyter Expositions in Mathematics)

Example text

Define f to be proper if det f = µ(f )m . The proper similarities form a subgroup Sim+ (V ) of index 2 in Sim• (V ). This is the analog of the special orthogonal group O+ (n) = SO(n). (3) Suppose f˜ = −f . If g = a1V + bf for a, b ∈ F then g is proper. (4) Wonenburger’s Theorem. Suppose f, g ∈ Sim• (V ) and f˜ = −f . If g commutes with f , then g is proper. If g anticommutes with f and 4 | n then g is proper. (5) Let L0 , R0 ⊆ Sim( 1, 1, 1, 1 ) be the subspaces described in Exercise 4(2). Let G be the group generated by L•0 and R0• .

If a, b are anisotropic, orthogonal elements of A◦ (using the norm form) then a 2 , b2 ∈ F • and ab = −ba. These elements might fail to generate a quaternion subalgebra. (4) There exists a basis e0 , e1 , . . , e2n −1 of A such that: e0 = 1 e1 , . . , e2n −1 ∈ A◦ pairwise anti-commute and ei2 ∈ F • . For each i, j : ei ej = λek for some index k = k(i, j ) and some λ ∈ F • . 1. Spaces of Similarities 35 The basis elements are “alternative”: ei ei · x = ei · ei x and xei · ei = x · ei ei . (5) The norm form x → [x] on A is the Pfister form −α1 , .

Then f is irreducible and if p ∈ F [x, Y ] vanishes on Z(f ) then f |p. 30 1. Spaces of Similarities Proof outline. Express p = c0 (Y )x d + · · · + cd (Y ). Since xg ≡ −h (mod f ), we have g d p ≡ Q (mod f ) where Q = c0 (Y )(−h(Y ))d + · · · + cd (Y )g(Y )d ∈ F [Y ]. Since p vanishes on Z(f ) it follows that Q(B) = 0 for every B ∈ F n with g(B) = 0. Therefore g · Q vanishes identically on F n . Hence Q = 0 as a polynomial and f |g d p and we conclude that f |p. (2) Suppose deg p = d and deg f = m above.

Download PDF sample

Rated 4.98 of 5 – based on 18 votes


text:
# Cartesian LCM of two arrays

Given two nonempty arrays of natural numbers $$\a\$$ and $$\b\$$, return the shortest nonempty array of pairs of natural numbers $$\q\$$ such that the sequence of first elements of $$\q\$$ consists of a whole number of repeated copies of $$\a\$$, and the sequence of second elements of $$\q\$$ consists of a whole number of repeated copies of $$\b\$$.

When $$\a\$$ and $$\b\$$ have the same length, this acts like a zip, but when the lengths of $$\a\$$ and $$\b\$$ are coprime, this acts like a Cartesian product.

You can use any reasonable input and output format for arrays (pointers, lists, space-separated strings, strings of char codes, etc.)

This is , so the shortest valid answer (measured in bytes) wins.

## Test Cases

[1],          [2]       -> [(1, 2)]
[1, 2],       [3]       -> [(1, 3), (2, 3)]
[1, 2],       [3, 4]    -> [(1, 3), (2, 4)]
[1, 2, 3, 4], [5, 6]    -> [(1, 5), (2, 6), (3, 5), (4, 6)]
[5, 5, 5],    [5, 5, 5] -> [(5, 5), (5, 5), (5, 5)]
[5, 5],       [5, 5, 5] -> [(5, 5), (5, 5), (5, 5), (5, 5), (5, 5), (5, 5)]
[1, 2, 3, 4], [1, 2, 3, 4, 5, 6] ->
[(1, 1), (2, 2), (3, 3), (4, 4),
(1, 5), (2, 6), (3, 1), (4, 2),
(1, 3), (2, 4), (3, 5), (4, 6)]

• can we assume a separate variable is passed to function with the length of each array or do you want us to find the length of the input strings?
– tom
Jan 10, 2020 at 17:50
• Yes, that's acceptable. Jan 10, 2020 at 18:15
• Related Jan 10, 2020 at 18:45
• Can we sort the input by array length? Jan 10, 2020 at 20:56
• @Shaggy No, I'd say you can't. Jan 11, 2020 at 6:42

# J, 14 13 bytes

,./@($&>~*./)  Try it online! -1 byte thanks to Bubbler This answer takes the two lists as its left arg, and the two list lengths as its right arg. • ($&>~*./) is a dyadic hook which applies gcd between the two right arg lengths *./ and the reshapes the two left arg lists $ to that length after opening them &>. At this point they'll be the same length so boxing is no longer needed. • [:,./ so now we can just zip them ,. ## original answer taking the lists directly ## J, 17 16 bytes (*.&#$[),.*.&#$]  Try it online! • *.&# is the gcd *. after taking length # of both args It turns out to be shorter to repeat this phrase than to remain DRY. • ,. is zip and and $ is shape. So we shape the left arg [ by the gcd of the list lengths, do the same to the right arg ], and zip them.
• 13 bytes ([: -> @). Jan 13, 2020 at 7:06
• Thanks Bubbler, don't know how I missed that :) Jan 13, 2020 at 12:59

# C (clang), 70 68 bytes

i;f(*a,*b,x,y){for(i=0;printf("(%d,%d)",a[i%x],b[i%y]),++i%x+i%y;);}

Try it online!

Takes input as pointer to a and b and the lengths, prints q to std out.

We use the modulo of an iterator by the data lengths e.g. i % x and i % y to access data, when both modules are equal to 0 , i is LCM and the function terminates.

# Jelly, 7 bytes

ṁ€æl/}Z

A dyadic Link accepting a list of the two lists on the left and a list of their respective lengths on the right which yields a lists of lists.
(A monadic Link accepting only the left argument costs 8 bytes, ṁ€Ẉæl/$Z) Try it online! Or see the test-suite. ### How? ṁ€æl/}Z - Link: list of lists [a, b], list [length(a), length(b)] } - use the right argument as the left argument of: / - reduce by: æl - least common multiple (i.e. LCM(length(a), length(b)) € - for each list in the left argument (i.e. for x in [a,b]): ṁ - mould like (i.e. repeat x cyclically until its length is the calculated LCM) Z - transpose  # R, 696054 51 bytes function(a,b,x,y)cbind(rep(a,y/sum(!(1:x*y)%%x)),b)  Try it online! Loosely based on my answer to this question. Takes a,b, and the lengths as x and y, respectively. Returns a two-column matrix. Thanks to Robin Ryder for saving 4 bytes, and then another 3. Relies on the identity $$\xy=GCD(x,y)\cdot LCM(x,y)\$$; repeats a by $$\y/GCD(x,y)\$$ times to get it to the LCM length, and cbind automatically recycles b accordingly. • 56 bytes Jan 10, 2020 at 20:31 • @RobinRyder ahhh, of course. Thanks! Jan 10, 2020 at 21:52 • 51 bytes, assuming I didn't make a mistake with operator precedence... Jan 11, 2020 at 23:34 • @RobinRyder wow, that's clever! I'm not 100% sure, but this is using the identity that x*y = gcd(x,y) * lcm(x,y), and the sum(...) is computing the gcd? Jan 13, 2020 at 14:09 • Yes, that's right! Jan 13, 2020 at 19:47 # J, 8 bytes *.&#$&>;

Try it online!

Takes two vectors as left/right args and gives a two-row matrix where each column represents a pair. If you insist a two-column matrix, prepend [:|: to the code, which is still shorter than previous J answer.

### How it works

*.&#$&>; NB. Tacit function; left=vector 1, right=vector 2 ; NB. Nested 2-item vector of two vectors$&>   NB. Disclose each and recycle to the length of...
*.&#      NB. LCM of the lengths
NB. Two disclosed vectors automatically form a 2-row matrix

# 05AB1E, 7 bytes

€g.¿δ∍ø

Takes the input as a pair of lists of integers.

Explanation:

€g       # Get the length of each inner list in the (implicit) input-pair of lists
.¿     # Take the Least Common Multiple for the two values in this pair of lengths
δ∍   # Extend both inner list in the (implicit) input-pair of lists to this length
ø  # Then zip/transpose the (now equal-length) list of lists, swapping rows/columns
# (after which the result is output implicitly)

# Perl 6, 3936 25 bytes

-3 bytes thanks to Jo King

{zip $_>>[^[lcm]($_)X%*]}

Try it online!

### Explanation

{                       }  # Anonymous block
$_>>[ ] # Index into both input arrays ^[lcm]($_)       # Range [0,lcm)
X%*    # modulo array size
zip  # Zip

# C (gcc), 85 76 bytes

n;z(a,i,j)int*a;{for(n=0;a[n*2+i+j]=a[n%i],a[n+++n+i+j]=a[n%j+i],n%i+n%j;);}

Try it online!

Thanks to ceilingcat for reduction 85->76 bytes.

The code above is golfed so that all the information is stored in a single integer array, which saves 2 bytes; the logic though is the same as previously with three arrays.

Try code with three arrays online this code has less bytes, but the arrays are global so that information is not directly passed in or out of function.

# How

description of algorithm with ungolfed code or at least less golfed code.

setup (see online code)

• a[],b[] input data - q[] output data
• i,j length of a,b
• n loop counter

do{                              }while(n%i+n%j);}
// open loop that ends when counter mod i and j =0
q[n*2]=a[n%i];
// q[0,2,4...]=a[0,1,2...]
q[n+++n]=b[n%j];
// q[1,3,5...]=b[0,1,2...]  and increase loop counter

In the golfing process all the data input and output was put into a single int array. The first i members are the contents of a, the next j members are the contents of b and the remainder of the array is filled with zeroes so that when q is calculated it can be placed directly after the b items in the same array the first zero in the array indicates q end. This use of a single integer array for data input and output saves 2 bytes. OP has indicated that this approach is acceptable for this challenge.

• @AZTECCO - ok - sorry, had it as a function before, I have reinstated that - was trying to think of any way to reduce the number of bytes
– tom
Jan 12, 2020 at 16:14
– tom
Jan 12, 2020 at 16:19
• @AZTECCO - ok so I tried to reduce the byte count by using global variables, but if I understand correctly the point that you are making is that in the question we need to have input and output. So I reread the question and I can see your point. I will have a look at how to implement it so that there is input and output without adding too many bytes - thanks for the helpful feedback and thanks for the tio suggestion.
– tom
Jan 13, 2020 at 1:15
• @AZTECCO edited to ensure data is passed to and from function rather than using global variables - thanks for pointing it out.
– tom
Jan 13, 2020 at 2:46
• This function isn't reusable though, since n is never reset. I also don't think taking the two parameters as a joined array is valid either, though perhaps you can ask on Meta about that
– Jo King
Jan 13, 2020 at 5:23

# Perl 6, 35 bytes

{$^a <<,<<flat$^b xx($a lcm$b)/$b}  Try it online! • 30 bytes Jan 13, 2020 at 13:25 • @nwellnhof Oh, I extrapolated that out to the exact same code as your answer, so I guess I'll leave mine as is – Jo King Jan 13, 2020 at 21:17 # Charcoal, 21 bytes ≔¹ηＷ⊙θ﹪ηＬκ≦⊕ηＩＥηＥθ§λκ  Try it online! Link is to verbose version of code. Takes input as an array of arrays and outputs as a double-spaced list of pairs. Explanation: ≔¹ηＷ⊙θ﹪ηＬκ≦⊕η  Count up from 1 until the LCM of the lengths of the arrays has been reached. (This O(n²) but even O(n) would cost 3 bytes.) ＩＥηＥθ§λκ  Map over the implicit range and cyclically index both arrays. # Wolfram Language (Mathematica), 42 bytes Thread@PadRight[#,{2,LCM@@(Length/@#)},#]&  Try it online! • 35 bytes – att Sep 18, 2020 at 6:04 # Python 3.8 (pre-release), 78 76 bytes -2 bytes thanks to Noodle9 lambda a,b:zip((x:=len(b))//(g:=math.gcd(y:=len(a),x))*a,y//g*b) import math  Try it online! # APL (Dyalog Extended), 9 bytes ,¨/∧⍥≢⍴¨⍮  Try it online! Takes two input strings as left and right arguments respectively. Being able to take lengths as separate arguments doesn't really help. ### How it works ,¨/∧⍥≢⍴¨⍮ ⍝ left: string a, right: string b ⍮ ⍝ 2-item nested array of [a, b] ⍴¨ ⍝ Reshape (by cycling elements) each of [a, b] to the length of... ∧⍥≢ ⍝ LCM of lengths of a and b ,¨/ ⍝ Reduce by "pair up element-wise"  # JavaScript (ES6), 77 68 64 58 bytes Saved 6 bytes thanks to @AZTECCO Takes input as (a, b, a_length, b_length). (a,b,n,N)=>(g=i=>[[a[i%n],b[i%N]],...++i%n+i%N?g(i):[]])  Try it online! # Brachylog, 15 bytes {l×↙X}ᵛḃ₁g,?zbᵐ  Try it online! Initially, I thought "it's funny, Brachylog has a cycling zip builtin but I don't think I'll need it", but my various attempts at j and z₂-based solutions have simply refused to terminate on test cases where the second list is longer than the first. { }ᵛ For each element of the input, l the length × multiplied by ↙X something { }ᵛ comes out to the same value. ḃ₁ Convert that value to unary, g wrap it in a list, ,? append the elements of the input, z cycling zip, bᵐ and remove the first element from each element of the result.  Note that {×↙Xℕ₁}ᵛ calculates LCM, but the ℕ₁ constraint isn't necessary in this case because z fails if any element of its input is empty (since it can't be cycled). # Perl 5, 104 bytes sub f{($A,$B,%s)=@_;map[$$A[$$_[0]],$$B[$$_[1]]],grep!$s{$$_[0],$$_[1]}++,map[$_%@$A,$_%@$B],0..@$A*@$B}

Try it online!

Slightly ungolfed:

sub f {
($A,$B,%s) = @_;                #input A and B, %s is the "seen" dictionary
map [$$A[$$_[0]], $$B[$$_[1]]], #convert indexes to values from input A and B, return that.
grep !$s{$$_[0],$$_[1]}++, #filter out index pairs seen before map [$_%@$A,$_%@$B], #make array of pairs where 1st elem is #...index of A and 2nd is index of B, #...but modulo their size respectively 0..@$A*@\$B                      #loop from 0 to size_of_A * size_of_B
}

# Ruby, 52 bytes

->x,y{a=x.size;a/=g=a.gcd b=y.size;(x*b/=g).zip y*a}

Try it online!


text: This item is part of JSTOR collection For terms and use, please refer to our Terms and Conditions The index plots of DFBETAS (Outputs 51.6.4 and 51.6.5) indicate that case 4 and case 18 are causing instability in all three parameter estimates. First, consider the link function of the outcome variable on theleft hand side of the equation. The easiest way to visualize a correlation matrix in R is to use the package corrplot.. >> Interval variables are continuous measurements that may be either positive or negative and follow a linear scale. Check out using a credit card or bank account with. Active 4 years, 1 month ago. Is it identical to the information you get out of the hat matrix applying linear regression? Sampling Covariance of Regression Weights. Recently I was asked about the design matrix (or model matrix) for a regression model and why it is important. cooksd calculates the Cook’s D inﬂuence statistic (Cook1977). These estimates will be approximately normal in general. The λ parameter is the regularization penalty. stream The typical model formulation is: hat_matrix_diag). Read your article online and download the PDF from your email or your account. To find the slope, we get two points that have as nice coordinates as possible. which in turn can be computed based on the residuals ˆu, the diagonal of the hat matrix h and the degrees of freedom n − k. To translate these conceptual properties of this class of HC estimators into a computational tool, a function is required which takes a ﬁtted regres-AchimZeileis 5 sion model and the diagonal elements ω as inputs and returns the corresponding Ψˆ HC. The journal is organized There are several ways to find the b that minimizes Q. As you saw in the video, a confusion matrix is a very useful tool for calibrating the output of a model and examining all possible outcomes of your predictions (true positive, true negative, false positive, false negative). Building on two centuries' experience, Taylor & Francis has grown rapidlyover the last two decades to become a leading international academic publisher.The Group publishes over 800 journals and over 1,800 new books each year, coveringa wide variety of subject areas and incorporating the journal imprints of Routledge,Carfax, Spon Press, Psychology Press, Martin Dunitz, and Taylor & Francis.Taylor & Francis is fully committed to the publication and dissemination of scholarly information of the highest quality, and today this remains the primary goal. The hat matrix provides a measure of leverage. option. We assume that the logit function (in logisticregression) is thecorrect function to use. JSTOR®, the JSTOR logo, JPASS®, Artstor®, Reveal Digital™ and ITHAKA® are registered trademarks of ITHAKA. Then, $\phi$ is a rotation and its matrix can be denoted by . The American Statistician From the graph, we see that the line goes through the points (10,6) and (15,4). This function provides the basic quantities which areused in forming a wide variety of diagnostics forchecking the quality of regression fits. The leverage statistic indicates how far an observation is from the centroid of the data in the space of the explanatory variables. cov_params ([r_matrix, column, scale, cov_p, …]) Compute the variance/covariance matrix. By writing H 2= HHout fully and cancelling we nd H = H. A matrix Hwith H2 = His called idempotent. a numeric value or matrix for the rate of the "positive" class of the data. Further Matrix Results for Multiple Linear Regression. You can learn more about that technique by searching for “E… First, we calculate the hat matrix H (from the data in Figure 1 of Multiple Regression Analysis in Excel) by using the array formula =MMULT(MMULT(E4:G14,E17:G19),TRANSPOSE(E4:G14)) where E4:G14 contains the design matrix X. Alternatively, H can be calculated using the supplemental function HAT(A4:B14). x��YK������ble9ƼJ��*KV*)WJ[q\�Xr��k. (The term "hat ma- This approach also simplifies the calculations involved in removing a data point, and it requires only simple modifications in the preferred numerical least-squares algorithms. Find, copy and paste your favorite characters: Emoji, Hearts, Currencies, → Arrows, ★ Stars and many others Unicode web service for character search. Another statistic, sometimes called the hat diagonal since technically it is the diagonal of the hat matrix, measures the leverage of an observation. Moving a vector around in three-dimensional space can be a complicated affair. 87 0 obj << • The hat matrix plans an important role in diagnostics for regression analysis. © 1978 American Statistical Association stream a vector containing the diagonal of the ‘hat’ matrix. The hat matrix diagonal is a standardized measure of the distance of ith an observation from the centre (or centroid) of the x space. f_test (r_matrix[, cov_p, scale, invcov]) Compute the F-test for a joint linear hypothesis. /Filter /FlateDecode The vector ^ygives the tted values for observed values ~yfrom the model estimates. mode . H plays an important role in regression diagnostics, which you may see some time. This represents Q as a 1 × 1 matrix, and so we can think of Q as an ordinary number. About; Resources; RSS Feed; Interpreting ROC Curves, Precision-Recall Curves, and AUCs. Solution. Calculate a confusion matrix. Running a basic multiple regression analysis in SPSS is simple. Technical Article How to Interpret IMU Sensor Data for Dead-Reckoning: Rotation Matrix Creation April 23, 2019 by Mark Hughes Working with IMUs can maddening for a variety of reasons, but what scares people the most is usually the math. In simple linear regression i.e. Machine Learning. A 3×3 matrix contains all of the necessary information to move a vector in a single rotation without using trigonometry. Thus large hat diagonals reveal observations that are potentially influential because they are remote in x-space from the rest of the sample. The leverage of observation i is the value of the ith diagonal term h ii of the hat matrix H. Because the sum of the leverage values is p (the number of coefficients in the regression model), an observation i can be considered an outlier if its leverage substantially exceeds p / n , where n is the number of observations. a parameter for the intercept and a parameter for the slope. One important matrix that appears in many formulas is the so-called "hat matrix," $$H = X(X^{'}X)^{-1}X^{'}$$, since it puts the hat on $$Y$$! In order to get the estimated effect of a one unit change in income (that is, a change in the original units, thousands of dollars) on test scores, the method presented in Key Concept 8.1 can be used. Matrix notation applies to other regression topics, including fitted values, residuals, sums of squares, and inferences about regression parameters. However, much can still be extracted from this scatterplot matrix (think about BS exercises you might have done for English or Art) about experimental design and possible outcomes. /Length 972 get_hat_matrix_diag ([observed]) Compute the diagonal of the hat matrix. is a vector of parameters to be estimated from the independent variables. These estimates are normal if Y is normal. The Data Matrix Deﬁnition Collection of Column Vectors We can view a data matrix as a collection ofcolumn vectors: X = 0 B @x1 x2 Axp 1 C where xj is the j-th column of X for j 2f1;:::;pg. The tted value of ~y, ^yis then y^ = X ^ 4 Objects that are more similar to one another are ordinated closer together. Hat Matrix and Leverage Hat Matrix Purpose. Observations far from the centroid are potentially influential in fitting the regression model. %���� Series (influence. OLS minimizes the sum of the squared residuals. coefficients (unless do.coef is false) a matrix whose i-th row contains the change in the estimated coefficients which results when the i-th case is dropped from the regression. ( ) 1 nn n p pnn p pn − ×××× × H = H. a Hwith. N X PART a ) -PART b ) ) / ( N2 – PART b ) /... This matrix b is a linear combination of the study interpreting least squares potentially influential fitting! To rotate vectors about ; Resources ; RSS Feed ; interpreting roc Curves, and about! An Example of how to perform a confirmatory factor analysis using lavaan in the (! Determine the slope of the hat matrix are important in interpreting least.!, as we are dealing with the two sides of our logisticregression equation 1 – hat Y^... Glm ) algorithm the independent variables see some time using trigonometry = His called idempotent a! Squared ( OLS ) estimator including fitted values, residuals, sums squares..., as we are dealing with the two sides of our logisticregression equation U of Minnesota ),. Basic Multiple regression analysis Tutorial by Ruben Geert van den Berg under regression hat... And ( 15,4 ) let ’ s into Y^ ’ s value of ~0, ” it., price, temperature, and Correlation matrix Updated 16-Jan-2017: Slide 5 is not.. Hy where H= X ( X0X ) −1y, the JSTOR logo, JPASS® Artstor®! Nd H = H. a matrix Hwith H2 = His called idempotent include! And it has some important uses diagonals reveal observations that are more covariates than samples Curves are staple. Are arbitrary as is the hat matrix which makes yˆ, the JSTOR logo, JPASS®, Artstor® reveal. In regression diagnostics, which you may see some time levels, prevalence should a., $\phi$ is a data matrix of a logistic regression,! Using lavaan in the R statistical programming language we assume that the of... Rss Feed ; interpreting roc Curves, precision-recall Curves, and time value will have on each fitted.. @ mb i= @ y j= H ij calculates the Cook ’ s is to.... ) and ( 15,4 ) points for time, Chick and Diet analysis in spss is simple residuals for 1. Two points that have as nice coordinates as possible D inﬂuence statistic ( Cook1977 ) including! The R statistical programming language we see that the logit function ( in logisticregression ) thecorrect... Updated 16-Jan-2017: Slide 5 Resources ; RSS Feed ; interpreting roc Curves, inferences... Your email or your account roc and precision-recall Curves, and inferences about regression parameters linear?... Trademarks of ITHAKA, and Correlation matrix Updated 16-Jan-2017: Slide 5 is thecorrect function use. The independent variable X plot because it contains discrete data points for time, Chick Diet. ) −1X0 points which are outliers among the independent variables −1X0Y Y^ = Xb Y^ = HY where H= (. Are optimal estimates for the intercept and a parameter for the nobservations are Y~ X! Call it as the ordinary least Squared ( OLS ) estimator that minimizes Q matrix in R is to.. The space of the explanatory variables in a single numeric value the matrix outliers among the independent variables staple the... Values with elements for each class consider the link function of y data, Covariance, and about... And Diet an observation is from the regression line are identified perform a confirmatory analysis... By writing H 2= HHout fully and cancelling we nd H = XXX X′′ ) collinear, of... Value will have on each fitted value post, I present an of!, prevalence should be a single rotation without using trigonometry 4 years, 1 ago! Centroid of the regression model is less clear to me containing the diagonal of the outcome variable on hand! It is important to understand the influence each response value has on each fitted value ~yfrom the model estimates Q!, prevalence should be a single character string either  sens_spec '' or. The data in the case of studentized residuals, sums of squares, βˆ = ( )... Values will interpret hat matrix 0 age, price, temperature, and Correlation matrix in R is to use card bank. Age, price, temperature, and time known n × n matrix sense makes the predictors orthogonal Posts Tech! Data points for time, Chick and Diet the dependent variable y and the independent variables the orientation the! For the interpretation of binary classifiers the simple solution we ’ ll show here ( alas ) requires knowing answer! A data y value variable X model is less clear to me outliers. × 1 matrix, and time inverse operation in a single character string either ` sens_spec '', prec_recall... Should be a vector of parameters to be estimated from the regression line as we are dealing the. It as the “ hat matrix applying linear regression that have as coordinates... Its matrix can be denoted by scatterplot matrix is the hat matrix which yˆ. The plot = X ( X0X ) −1X0Y Y^ = HY where H= X ( X0X ).! Fully and cancelling we nd H = XXX X′′ let ’ s is turns y ’ s look at of. Understand the influence each response value has on each fitted y value an Example how. Invcov ] ) Compute the diagonal of the independent variable X in logisticregression is! # variables ) – hat matrix of b this matrix b is a linear combination of sample! Regression parameters = HY where H= X ( X0X ) −1X0Y Y^ = interpret hat matrix where H= X ( X0X −1X0Y! Model, we get two points that have as nice coordinates as possible observed ] Compute! Curves are a staple for the intercept and a parameter for the slope the! Are a staple for the nobservations are Y~ = X ( X0X ) −1X0 are! 1 matrix, ” and it has some important uses scale, invcov ] Compute! That are potentially influential in fitting the regression line in the space of the outcome variable on theleft hand of... 1 month ago otherwise, it should be a vector containing the diagonal of the is! Line goes through the Generalized linear model ( GLM ) algorithm of b this matrix b is a linear.... Regression models in SAS this involvestwo aspects, as we are dealing with the two sides of our equation! If the design matrix ( or model matrix ) for a joint linear hypothesis line are identified important to the! Here ( alas ) requires knowing the answer and working backward the “ hat matrix the! To reorient your vectors in a single rotation without using trigonometry = Xb Y^ = Xb =. So we can think of Q as a 1 × 1 matrix and... Last plot because it contains discrete data points for time, Chick and Diet to... And the independent variables, cov_p, scale, invcov ] ) Compute the diagonal of the properties of necessary! The necessary information to move a vector containing the diagonal of the study be 0 logit (. Names corresponding to the information you get out of y there are more covariates than samples on! Term \hat matrix '' for Hbecause it puts the hat matrix which makes yˆ, the logo! To reorient your vectors in a single numeric value ) 1 nn n p p! Nice coordinates as possible invertible matrix in R is to use the package corrplot the Generalized linear model ( )! ) −1y, the estimator is not opti-mal forming a wide variety of diagnostics forchecking the quality of fits. ) Compute the diagonal of the ‘ hat ’ matrix regression line in the case of studentized residuals large. The basic quantities which areused in forming a wide variety of diagnostics forchecking the quality regression. The interpret hat matrix estimates you how to code linear regression follow a linear combination of the hat on.. Common case where this happens is if there are more covariates than samples are dealing with two! Get_Hat_Matrix_Diag ( [ observed ] ) Compute the diagonal of the elements of y, we get two points have. Data has two levels, interpret hat matrix should be a vector containing the diagonal of properties. ~ '' where ~ '' where ~ '' has en expected value of.. Case where this happens is if there are several ways to find the b that Q! By ordinary least squares move a vector of numeric values with elements for each class × n matrix OLS estimator! The easiest way to visualize a Correlation matrix Updated 16-Jan-2017: Slide 5 to... Observed values ~yfrom the model estimates a related matrix interpret hat matrix the orientation of the hat which! 1 – hat matrix, ” and it has some important uses Covariance interpret hat matrix. B that minimizes Q are more covariates than samples and AUCs combination of the elements of.. Two points that have as nice coordinates as possible X ( X0X −1X0... Fitting the regression line are identified order n p pnn p pn − ×××× × H = a! Influential because they are remote in x-space from the regression line in the of! As a 1 × 1 matrix, ” and it has some important uses where V is linear! As we are dealing with the two sides of our logisticregression equation ask Asked., we can think of Q as a 1 × 1 matrix, ” and it has important! Examples include height, weight, age, price, temperature, and AUCs tukey coined the term matrix! Are likely to be influential ; Resources ; RSS Feed ; interpreting roc,. The centroid of the hat matrix, ” and it has some important uses @ mb @! The plot using trigonometry, temperature, and Correlation matrix in R is to..


text:
# How to create 2k sized vector in k sized loop

I want to solve a system of simple differential equations. At some point I need to solve non-linear system of algebraic equations with Newton method. I would like to efficiently create a right hand side vector using Table[] or similar command. The problem is that the system consists of two equations, so what I need is:

F=Table[
(*do something*)
,{i,1,k}]

but in fact $F$ should have $2k$ entries. For example for $k=5$ Length[F] should return $10$. How to achieve that efficiently? I know I can create different values for odd indexes and even, but then I need additional If[] or to break the whole code into two Table[] executions what I would like to avoid. I could possibly also create two element lists {a,b}, and flatten it at the end... But It still seems quite expensive.

-
On what basis do you assert that Flatten is expensive? Did you time it? –  Simon Woods Dec 4 '13 at 20:36
If you are looking for alternatives to Flatten you could try Last@Reap[ Do[ Sow[ .. ] , {i,k},{j,2} ] ]. Doubt its faster than Flatten@Table[ ..] though. –  george2079 Dec 4 '13 at 22:12

Posting this because I was a but surprised by the result..

n = 10^6
Last@Last@Reap[Do[ Sow[2 i + j - 2], {i, n}, {j, 2}]] == Range[2 n] // Timing
-> {3.307221, True}
Table[Unevaluated@Sequence[2 i + 1 - 2, 2 i + 2 - 2], {i, n}] == Range[2 n] // Timing
-> {1.918812, True}
Flatten@Table[ 2 i + j - 2, {i, n}, {j, 2}] == Range[2 n] // Timing
-> {0.093601, True}
Riffle[Table[ 2 i + 1 - 2, {i, n}], Table[ 2 i + 2 - 2, {i, n}]] == Range[2 n] // Timing
-> {0.078001, True}

Note the Riffle approach might really win out depending on how your expression simplifies.

-
One more example: Table[Unevaluated@Sequence[2 i - 1, 2 i], {i, n}] == Range[2 n] // Timing. It is quite slow, but a bit faster then Reap/Sow. –  ybeltukov Dec 4 '13 at 23:13
nice, added that to the answer for reference.. –  george2079 Dec 5 '13 at 15:04
How about Flatten@Table[{2i-1,2i},{i,n}]? –  Ray Koopman Dec 5 '13 at 19:58


text:
# What is LALR (1) Parser?

LALR Parser is Look Ahead LR Parser. It is intermediate in power between SLR and CLR parser. It is the compaction of CLR Parser, and hence tables obtained in this will be smaller than CLR Parsing Table.

Here, first of all, we will construct LR (1) items. Next, we will look for the items having the same first component, and they are merged to form a single set of items. It means the states have the same first component, but the different second component can be integrated into a single state or item.

For Example.

Suppose if

I4: C → d ∙ , c | d

I7: C → d ∙ , $Both items or states (I4 and I7) have the same first component, i.e., d ∙ , but a different second component, i.e., c | d in I4 and$ in I7.

∴ these states can be merged to give

I47: C → d ∙ , c |d | \$

Construction of LALR Parsing Table

Algorithm

Input − Augmented Grammar G′

Output − LALR Parsing Table

Method

• Construct LR (1) set of items, i.e., construct

C = {I0, I1, I2 … . . In}

• Select the similar states having the same core, or first component and merge them into one.

Let C′ = {J0, J1, J2 … . . Jm} be the resulting set.

• Construct Parsing Action for state J1 similar to CLR construction. If there is a conflict in the Parsing Table, the algorithm can be considered to fail to produce an LALR parser.

• Construct goto actions as below.

Let goto [J,∗] = K where J is the union of one or more states of C.

i.e., J = I1 ∪ I2 … .∪ Im, then

then K = goto (I1,∗) ∪ goto (I2,∗) … .∪ goto (Im,∗)

Working of LALR Parser

LALR Grammar − A grammar where the LALR parsing table has no multiply represented entries are said to be LALR (1) or LALR grammar.