text:
## Impredicative Encodings, Part 3

In this post I will argue that, improving on previous work of Awodey-Frey-Speight, (higher) inductive types can be defined using impredicative encodings with their full dependent induction principles — in particular, eliminating into all type families without any truncation hypotheses — in ordinary (impredicative) Book HoTT without any further bells or whistles. But before explaining that and what it means, let me review the state of the art.

Categorically, a (higher) inductive type is an initial object in some category. For instance, the coproduct of $A$ and $B$ is the initial object of the category of types $X$ equipped with maps $A\to X$ and $B\to X$; and the circle $S^1$ is the initial object of the category of types $X$ equipped with a point $b:X$ and an equality $l:b=_X b$. A (H)IT is therefore a kind of “colimity” thing, while an “impredicative encoding” of it is a way to construct it (or an approximation thereof) using limits instead — specifically, large limits, which requires a universe closed under impredicative quantification (i.e. $\Pi$-types whose domain is not necessarily an element of the universe).

The most basic such encodings (usually associated with System F) approximate the initial object of a category by the product of all objects of that category. For instance, the System F coproduct $A+B$ is the product of all types $X$ equipped with maps $A\to X$ and $B\to X$, which in type-theoretic syntax becomes

$\prod_{X:\mathcal{U}} (A\to X)\to (B\to X) \to X.$

Such impredicative encodings of ordinary inductive types are well-known in type theory, and back when we were first discovering HITs I blogged here about the fact that they can also be encoded impredicatively. However, these basic encodings have the problem that they don’t satisfy the “uniqueness principle” or $\eta$-conversion, and (equivalently) they don’t support a “dependent eliminator” or “induction principle”, only the non-dependent “recursion principle”. In categorical language, the product of all objects of a category, even if it exists, is only a weak initial object.

Last year, Sam Speight blogged here about a way to fix this problem (paper here with Awodey and Frey), by defining a (higher) inductive type to be the limit of the identity functor of the category in question, and appealing to this theorem. Such a limit, if constructed out of products and equalizers, appears as a subobject of the product of all objects; and if we “compile out” this definition in type theory, it adds additional assertions that System F encoding data is natural. For instance, the coproduct becomes

$\sum_{\alpha:\prod_{X:\mathsf{Set}_{\mathcal{U}}} (A\to X)\to (B\to X) \to X} \prod_{X,Y:\mathsf{Set}_{\mathcal{U}}} \prod_{f:X\to Y} \prod_{h:A\to X} \prod_{k:B\to X} f(\alpha_X(h,k)) = \alpha_Y(f\circ h, f\circ k).$

This approach is very nice, but unfortunately it only works for h-sets, i.e. 0-types. That is, given two sets $A,B$, it produces a coproduct set $A+B$, which has a dependent induction principle that can only eliminate into other sets. Categorically, the point is that the construction of limits out of products and equalizers works in a 1-category, but not in a higher category. We can boost up the dimension one at a time by adding additional coherence conditions — the paper ends with an example of $S^1$ constructed as a 1-type with a dependent induction principle that can eliminate into other 1-types (but not higher types) — but this approach offers no hope of an induction principle into types that are not $n$-truncated for any $n$. If we could solve the “problem of infinite objects” (perhaps by working in a context like two-level type theory) maybe we could add “all the coherence conditions at once”, although the path algebra would probably get quite hairy.

Surprisingly (to me), it turns out that there is a different solution, which works in (impredicative) Book HoTT without any bells or whistles. Recall that theorem about initial objects as limits of identity functors, and note that it’s proven using this lemma, which says that if $I$ is an object of a category equipped with a natural transformation from the constant functor $\Delta I$ to the identity functor, i.e. a cone consisting of maps $p_X:I\to X$ for all objects $X$ such that $f\circ p_X = p_Y$ for all morphisms $f:X\to Y$, and moreover $p_I:I\to I$ is the identity morphism, then $I$ is initial. Can we use this lemma directly?

You might think this is no better, since even obtaining a fully-coherent $\infty$-natural transformation $p_X:I\to X$ already involves infinitely many coherence conditions. However, inspecting the proof of this lemma, we see that it will work in HoTT even for an “incoherent” natural transformation, essentially because the definition of contractibility is a propositions-as-types translation of being a singleton set. That is, to show that $I$ is initial in $\mathcal{C}$, we want to show that $\hom_{\mathcal{C}}(I,X)$ is contractible. We take its center to be $p_X$, and then we must show that any $f:I\to X$ is equal to $p_X$. But by incoherent naturality, we have $p_X = f\circ p_I$, which is equal to $f$ since $p_I = \mathsf{id}_I$.

This is great, because the 0-type version of the Awodey-Frey-Speight construction, if written down with the full universe $\mathcal{U}$ in place of $\mathsf{Set}_{\mathcal{U}}$, already comes with an incoherent cone over the identity functor. So “all” we need to do is ensure $p_I = \mathsf{id}_I$. (Note that this is a version of $\eta$ for an inductive type.)

Here’s the trick. Note that the proof of the lemma shows $I$ is initial by applying the naturality property in a case where one of the objects is $I$ itself. Let’s try to prove $p_I$ is the identity by applying that same naturality property in the case where the morphism is $p_I:I\to I$ itself. This gives us $p_I \circ p_I = p_I$. In other words, although $p_I$ may not (yet) be the identity, it’s already the next best thing: an idempotent. And in the words of Robinson and Rosolini,

No category theorist can see an idempotent without feeling the urge to split it.

This is especially true when we were hoping that that idempotent would turn out to be an identity, since splitting it is a way to “make” it an identity. And in fact it’s not hard to show with categorical algebra that if $r:I\to J$ and $s:J\to I$ are a splitting of $p_I$ (so that $s r = p_I$ and $r s = \mathsf{id}_J$), where $p_X:I\to X$ is a cone over the identity functor, then $J$ is initial. For we have another cone $p_X s : J\to X$, whose $J$-component is $p_J s$. And we have $p_J = r s p_J = r p_I = r s r = r$, using naturality $s p_J = p_I$ and the splitting equations, so $p_J s = r s = \mathsf{id}_J$, so the lemma applies. Note that this argument also uses no higher coherence, and so should work just fine for an incoherent natural transformation.

What’s left is to split the idempotent $p_I$ in type theory. Fortunately, I wrote a paper a few years ago (original blog posts here and here) about precisely this problem, inspired by analogous results of Lurie in higher category theory. It turns out that an arbitrary “incoherent idempotent” (a map $q$ equipped with an equality $q\circ q = q$) may not be splittable, but as soon as the “witness of idempotency” $h: q\circ q = q$ satisfies one additional coherence condition (not the infinite tower of such one might expect), the map $q$ can be split. And in our situation, we can obtain this one additional coherence condition for the naturality triangle $p_I \circ p_I = p_I$ by using the 1-type version of the Awodey-Frey-Speight construction. (Actually, we can even omit their unit condition; all we need is the composition coherence for pseudonaturality.)

I’ve verified in Coq that this works for coproducts, using type-in-type for impredicativity. (I don’t think Coq’s built-in impredicative-set option is compatible with the HoTT library, which has tried to excise Coq’s built-in smallest universe Set as much as possible.) Most of the proof is quite easy; the longest part (40 lines of path algebra) is deducing the idempotence coherence condition from the naturality coherence condition. As expected, we only get typal computation rules for the induction principle — although we do have definitional computation rules for the recursion principle (i.e. the non-dependent eliminator). More precisely, there is a non-dependent eliminator (a special one, not just the dependent eliminator specialized to a non-dependent motive) that satisfies a definitional computation rule.

I’m working on coding it up for higher inductive types as well, but the path algebra gets quite annoying. Further bulletins as events warrant.

To conclude, let me point out that I find this a very satisfying answer to the question with which I ended my second idempotents post:

… [For equivalences] we also have a “fully coherent” notion $\mathsf{IsEquiv}(f)$… that is a retract of a type $\mathsf{QInv}(f)$ of “partially coherent” objects…. Are there any other structures that behave like this? Are there any other “fully coherent” gadgets that we can obtain by splitting an idempotent on a type of partially-coherent ones?

The answer is yes: a fully-coherent impredicative encoding can be obtained by splitting an idempotent on a partially-coherent one.

This entry was posted in Foundations, Higher Inductive Types. Bookmark the permalink.

### 50 Responses to Impredicative Encodings, Part 3

1. Mike Shulman says:

Hmm, apparently wordpress posted this for me even though I wasn’t quite ready yet. I intended to add the remark that this construction of (H)ITs requires that we already have the natural numbers, which are used in the construction of idempotent splitting. So we can’t use it to define the natural numbers impredicatively. I also don’t know how generally it will work for other recursive HITs: I don’t immediately see an obstacle, but if it works for “LS section 9” then that would mean that impredicativity is more powerful than I ever realized.

• Mike Shulman says:

Oh, and I also meant to add that we need function extensionality. Of course that was already true for the Awodey-Frey-Speight version, but it’s “even more true” here because idempotent-splitting also requires function extensionality.

Univalence, however, is not required.

2. Steve Awodey says:

Wow – fantastic!
This should open up all kinds of possibilities.

3. Mike Shulman says:

Yes — here’s one additional, slightly different, possibility that just occurred to me. Suppose we have a subuniverse $\mathcal{U}_L \subseteq \mathcal{U}$ that we’d like to show is reflective. If it consists of the $f$-local types for some $f$, then we can express this as a HIT localization and impredicatively encode the latter. But in fact, as soon as $\mathcal{U}_L$ is closed under limits (which is always true for the $f$-local types), we should be able to reason more directly, starting from the naive impredicative encoding

$L X = \prod_{Y:\mathcal{U}_L} (X\to Y) \to Y$

refining it a la AFS:

$\sum_{\alpha:\prod_{Y:\mathcal{U}_L} (X\to Y)\to Y} \prod_{Y,Z:\mathcal{U}_L}\prod_{f:Y\to Z} \prod_{g:X\to Y} f(\alpha_Y(g)) = \alpha_Z(f\circ g)$

adding an extra level of coherence, then splitting an idempotent. So in impredicative HoTT, every subuniverse closed under limits should be reflective (i.e. we have the “dream adjoint functor theorem”).

• Steve Awodey says:

Yup – this should also work the same way for algebras for endofunctors, since they’re also closed under limits, which are created by the forgetful functor. We do the set-level W-types this way in our paper, but now it should also work for arbitrary (polynomial) endofunctors. Similarly, I guess we can also prove the “dream fixed-point theorem”: every endofunctor $F : \mathcal{U} \to \mathcal{U}$ has a (“least”) fixed point.

• Mike Shulman says:

In particular, the dream adjoint functor theorem should allow us to localize at large families of morphisms, which ordinary HITs do not. For instance, in this way we should be able to construct the hypercompletion modality, as well as homotopical localization and completion with respect to homology and cohomology theories. The latter are standard tools of classical algebraic topology, but so far we have not managed to construct them in HoTT; classically one only finds a small generating set by a cellular cardinality argument.

• Dan Christensen says:

Very nice! About the classical situation: we don’t know whether we can localize with respect to an arbitrary cohomology theory, unless we assume Vopenka’s principle. (Some references are at https://ncatlab.org/nlab/show/cohomology+localization) Is there a relationship between impredicativity and such large cardinal axioms?

4. Mike Shulman says:

However, there is a serious issue remaining with this approach to HITs (which may be related to Dan’s question about cohomological localization). A HIT constructed impredicatively with this construction can eliminate into types of unbounded h-level, but still only ones that belong to the impredicative universe. In particular, it can’t eliminate into the impredicative universe itself. However, in order to prove much of anything about a HIT (e.g. with encode-decode) we need it to eliminate into some univalent universe!

I think I recall that it’s inconsistent for one impredicative universe to contain another one. In impredicative Coq, the impredicative universe is the smallest universe; is there any other choice? Is it consistent for an impredicative universe to contain a predicative one? If not, then we may not actually be able to prove very much about these impredicative HITs.

• Matt Oliveri says:

Is it consistent for an impredicative universe to contain a predicative one?

Fiddling around with impredicative universes is one thing I eventually want to try. My intuition is that what’s really going on is you need to keep straight which function types are for functional programs, and which are for functional relations. With Coq’s -impredicative-set, Set‘s function types are for programs, and Type‘s function types are for anafunctions. I think you could put “predicative” universes inside impredicative Set as long as you realize that the functions still can’t be anafunctions, because you want cumulativity.

My hope was to use modes to enforce program/relation, instead of universe level, and give all the universes impredicative quantifiers! Caveat: The impredicative quantifiers themselves need to be anafunctions, but their elements cannot be.

But this may not be the only/best way to think about it. It may also be dead wrong, since I haven’t actually worked out details. Also, this thinking is all rather assemblies-ish. My impression was that toposes don’t play nice with proof-relevant impredicative quantifiers. And HoTT is supposed to be topos-like.

On the other hand, what I’m calling “anafunctions” are just those things that work like anafunctions from the metalanguage’s perspective. With honestly predicative HoTT, the functions all internally behave like anafunctions, but externally, they can be plain old programs. Maybe that can work to some extent with an impredicative HoTT too.

• Steve Awodey says:

An impredicative universe can (and does) contain a predicative one: from the type of natural numbers one can construct a universe $\tilde{F}\to F$ of finite sets in the usual way. Then one can even make it univalent by forming the “pregroupoid” $\mathbb{F}$ of finite sets, and then using an impredicative encoding to make the groupoid quotient (aka Rezk completion) $B(\mathbb{F})$, which will be (the indexing type of) a univalent universe $E \to B(\mathbb{F})$ with Sigma-, Pi-, and Id-types.

• Mike Shulman says:

Hmm… but the groupoid quotient is a HIT, so it seems that the only way to characterize its identity types (and show that your universe is univalent) is if we could already eliminate from it into a univalent universe?

• Steve Awodey says:

Let me get caught up – there’s already a lot going on here:
– yes the groupoid quotient is a HIT, but the idea is to make it by an impredicative encoding, like you can make a set-quotient by an impredicative encoding (I don’t want to write it out here, but I think you can imagine how it goes: homming out of the quotient has a universal property that can be unwound in the impredicative encoding).
– I don’t know what you mean by “to characterize the identity types you need to eliminate into a univalent universe”. Maybe you are not thinking of doing it impredicatively, but instead by forming the usual HIT? Either way, we do have the big impredicative universe which we might as well assume is univalent.
– we can separate the issue of impredicative encoding of groupoid quotients from making a predicative universe inside an impredicative one. Which part are you not happy with?

• Mike Shulman says:

Yes, I assumed you meant to make the groupoid quotient by an impredicative encoding; that shouldn’t be a problem. Such a groupoid quotient would have the right universal property, but to show that it actually defines a univalent universe would still require characterizing its identity types (to prove univalence), presumably using an encode-decode along the lines of Step 3 of the second proof of Theorem 9.9.5 in the book. We can assume the big impredicative universe is univalent, but that doesn’t help because the groupoid quotient, like all the other impredicatively defined HITs, can’t eliminate into the big impredicative universe, only to types inside of it.

Put differently: if all we know is that we have one univalent impredicative universe (and perhaps other larger univalent universes containing it, but no HITs in the ordinary sense), then there’s nothing to prevent all types inside that impredicative universe from being sets. In that case the impredicatively defined HITs would still have the right universal property for eliminating into other types in the impredicative universe, which is all you get out of their construction; but globally, they would be more like the 0-truncation of the HITs we really want.

• Matt Oliveri says:

Yeah, to actually do a predicative universe construction inside the type theory, I’m pretty sure you need large elimination.

That’s the big remaining problem with the impredicative encodings of this post: that they still don’t provide large elimination.

• Steve Awodey says:

I don’t really see the problem. As we say in the paper, *some* of the things that conventional wisdom says require large elims can actually be done differently. For example, we get the dependent elim from simple elim via the eta rules. So are you saying that the result might fail to be a *universe* (how could that be — it’s a universe for everything that it classifies), or that might fail to be univalent — i.e. to have the universal property of a groupoid quotient? The latter holds if the impredicative encoding works right to give the eta rules, which I think we agree is ok.
So it seems that the issue is just whether it has the right universal property with regard to large types, like the universe itself — which of course it won’t necessarily have. But then the question is again, for what do we need that?

• Mike Shulman says:

I’m saying it can fail to be univalent. The universal property of a HIT groupoid quotient is different from saying that the quotient is univalent. The universal property is a “mapping out” property; it doesn’t tell you what the identity types of the object are, and in particular not about univalence, until you have some kind of large elims. Just like the unit type has the universal property of $S^1$ in the category of sets; the universal property of $S^1$ only tells you that $\pi_1(S^1)=\mathbb{Z}$ once you have large elims into a univalent universe.

• Steve Awodey says:

Being univalent for a pre-groupoid just means that it is a 1-type and its pre-groupoid structure is its identity type. The universal property implies that the quotient is a 1-type, so it does indeed say something about the identity types — namely that they are (at most) sets. Are you saying that we don’t know that the quotient actually is a *proper* 1-type because we don’t know whether there are any (other) proper 1-types? We don’t need the universe for this.

• Mike Shulman says:

That’s right: for all we know, the “groupoid quotient” might actually be a 0-type. I suppose technically we might not need a universe, but univalence is the only axiom I know of that guarantees that non-0-types exist, and encode-decode into a univalent universe (and related arguments) is the only way I know of to prove that a particular type is not a 0-type and characterize its identity types.

• Mike Shulman says:

I can see how this argument might be modified to show in a hypothetical model that a universe of “modest $\infty$-groupoids” contains a univalent universe of finite sets.

However, I think a univalent universe containing only finite sets is of limited usefulness. In particular, in order to show something like $\pi_1(S^1)=\mathbb{Z}$ we need to eliminate from $S^1$ into a univalent universe that contains $\mathbb{Z}$.

• Steve Awodey says:

I was just giving an example to answer your question of whether it is consistent to have a (univalent) predicative universe inside an impredicative (univalent) one. If you now want a bigger one, we can look for that, too : – )
Anyway, I think it’s better to have the impredicative universe at the “top”, rather than at the bottom of a hierarchy of predicative universes.

• Mike Shulman says:

Maybe if we built an impredicative universe of modest $\infty$-groupoids based on a PCA of inaccessible cardinality? (-:O

• Steve Awodey says:

Maybe … I haven’t considered such things. But I don’t see any reason why we can’t have a small predicative universe containing the natural numbers in the big impredicative one.

• Mike Shulman says:

That’s what I was trying to imagine how to construct. An obvious set-theoretic point of view is that a universe containing the natural numbers must be inaccessibly large, so I was trying to imagine how such a thing could sit inside a universe of modest things.

• Matt Oliveri says:

Quite-comfortable predicative universes work with modest sets based on a countable PCA. This is essentially what the semantics of Nuprl’s CTT has. I think this is also how universes work in Feferman’s explicit mathematics.

The trick is to have type codes as programs of the PCA, separately have “semantic types” as modest sets or whatever, then relate them by a partial interpretation function. The partial interpretation is outside the PCA, but the type codes give you a way to handle types from within. Since the predicative universes really are predicative, you can just define them one after another, using the partial interpretation functions as the modest sets for the universes themselves.

From a size perspective, having all sorts of pretoposes as universes doesn’t seem problematic, but the programs of the PCA aren’t really relations.

• Mike Shulman says:

Oh, I think I see how that might work; thanks! And Harper et. al.’s computational cubical type theory is built on a PCA like that too, right? So their PER model, with all its univalent universes, ought to live inside an impredicative universe of modest objects in an ambient “realizability $\infty$-topos”. Nice!

• Matt Oliveri says:

Well, computational cubical type theory seems more like a PCA-based model category for a predicative HoTT. So in terms of size, your OK, but I don’t know off hand how to get the predicative universes to agree with the impredicative one about paths. Maybe it’s easy, or hard, or impossible.

Do we even know for sure that a proof-relevant, impredicative universe is consistent with, say, propositional truncation? (Including the consequent unique choice principle?) I repeat that my impression was that a proof-relevant impredicative universe doesn’t work in a topos. But I’m fuzzy on the details. Maybe the situation is that proof-relevant quantifiers range only over projective objects?

• Steve Awodey says:

The modest sets in the assemblies on a pca are an example of a proof-relevant, impredicative universe in a setting with propositional truncation, since the category of assemblies is regular.

• Matt Oliveri says:

Yes, but the notion of proposition in assemblies is different from HoTT: you can’t prove unique choice. Well, semantically I’d rather think that’s because the notion of function is different. Unique choice collapses functions and anafunctions.

• Steve Awodey says:

I have no idea what you mean. There’s no non-trivial HoTT in assemblies, because everything is a 0-type. The notion of a proposition in a regular category is defined by image factorization. There’s no room for anything to be “different” here. This is an example of an impredicative, proof relevant universe in a setting with propositional truncation (period). The only way around that is by interpreting something in a non-standard way.

• Mike Shulman says:

Nothing forces you to use functions rather than anafunctions just because you’re talking about assemblies or PERs. The computational type theory people seem to prefer functions, but I believe that if you define modest sets inside a realizability topos, the notion of “function” you get is an anafunction, and they’re still impredicative.

• Steve Awodey says:

Wait: the question was whether it is *consistent* to have a proof relevant, impredicative universe in a setting with propositional truncation. I gave an example of one. Whether blah, blah, anafunctions, blah, blah is a red herring.

• Mike Shulman says:

I certainly agree with that, if “proof relevant universe” means “a universe containing non-hprops”. My response was to Matt, not to you; I was trying to explain why this example is different from how he seems to expect assemblies to behave (and in particular, has unique choice): namely, because it uses “anafunctions” (the definition of morphisms in a realizability topos).

• Steve Awodey says:

The question was whether it’s consistent to have a proof-relevant, impredicative universe in a setting with propositional truncation. The example I gave shows that it is.

• Mike Shulman says:

My response was to Matt, not to you. I agree that your example shows that; I was trying to explain why this example behaves differently than he seems to expect assemblies to behave.

• Matt Oliveri says:

To reply to both of you, maybe I should back up and state some assumptions: We want an impredicative universe, whose type theoretic axiomatization is the same as for the PERs/modest sets within the category of assemblies. But we also want propositional truncation, whose axiomatization is like in Book HoTT.

So my concern is whether that actually has a model anyone knows of. By subsetting the impredicative universe to its h-props, it seems like you should get a subobject classifier. But I thought the category of assemblies doesn’t have a subobject classifier, and so we may be confusing what we have a model for.

In assemblies or PERs/modest sets, you have a distinction between functions and anafunctions. With a subobject classifier, you have unique choice and you don’t have a distinction between functions and anafunctions. Yes of course, with assemblies you can use anafunctions, but to use assemblies, you need to chuck out unique choice.

Maybe the confusing part is that in Book HoTT, we didn’t need to do anything special to get unique choice. But I think that just means Book HoTT’s propositional truncation is not a correct axiomatization of bracket types for assemblies.

• Mike Shulman says:

In the internal type theory of a realizability topos, which is the model Steve is talking about, there is an impredicative subobject classifier (an impredicative universe of all hprops) and also a proof-relevant impredicative universe of modest sets. The morphisms between the modest sets (and indeed between all objects, which are rather more general) in this model are, by definition, what one might call “anafunctions”. Unique choice holds globally; the model doesn’t know anything about the “non-ana functions”. However, I believe that not every hprop is modest: the impredicative universe of all hprops is not a subtype of the proof-relevant impredicative universe of modest sets.

• Steve Awodey says:

This column is getting pretty skinny, but I’ll give it a try:
To show that the modest sets are closed under subjects in the topos, we can use the characterization of the modest sets as the right orthogonal class of $\Omega \to 1$. An easy diagram chase shows that that class is closed under subobjects.

• Mike Shulman says:

Oh, okay, that’s nice to know. I guess the only caveat then is that the subobject classifier itself is not modest (which is, of course, impossible, since one impredicative universe cannot contain another one).

• Matt Oliveri says:

Steve referred to the category of assemblies on some PCA. I knew most of what you say about the corresponding realizability topos. The part that concerns me is whether the modest sets still count as impredicative in the right way, as a universe for the whole topos, rather than just the assemblies. The CIC-style axiomatization of an impredicative universe is supposed to be for the category of assemblies. I don’t know if it works for the topos. (But maybe it does. That’s just what I’ve been worrying about this whole time.)

• Mike Shulman says:

I believe this is the point of the Hyland-Robinson-Rosolini paper The discrete objects in the effective topos.

• Steve Awodey says:

Moving out from Mike’s last, very skinny, comment about whether large elim into a univalent universe is needed:
Ok, now I think I see your point — it’s not that we *need* a univalent universe, just that the known proof uses one. I agree with that, but I don’t think it’s a problem. The modest Kan cubical assemblies, e.g., include plenty of higher types.

• Mike Shulman says:

Okay, so you are thinking about models. I must have misunderstood your first post about the groupoid quotient; I thought you were proposing that we could construct a univalent universe of finite sets inside an impredicative one inside of type theory. I am certainly convinced by your argument that such things should exist in models.

• Steve Awodey says:

Maybe the discussion moved off in a different direction, but the original question was whether it is *consistent* to have a predicative (and perhaps univalent) universe inside an impredicative one. That’s what the example was supposed to show — not that it’s *provable* that there are such things.

5. Matt Oliveri says:

So by impredicative Book HoTT, it looks like you *don’t* mean Book HoTT with propositional resizing. For that system, maybe I’m being thick, but it seems like none of this would actually be impredicative, since the quantifiers are not yielding propositions. So it probably wouldn’t work.

So does impredicative Book HoTT mean same axioms, but with -impredicative-set? I don’t understand the technical reason to test this with -type-in-type. Doesn’t impredicative Set support everything that regular Set does?

• Mike Shulman says:

Right, propositional resizing is a totally different kind of “impredicativity”. (They overlap in permitting impredicative definitions of propositional truncation, though, as well as things like truncated disjunction and existential quantifiers.)

As I said in the post,

I don’t think Coq’s built-in impredicative-set option is compatible with the HoTT library, which has tried to excise Coq’s built-in smallest universe Set as much as possible.

• Mike Shulman says:

Maybe you’re asking for more details on that last point? I don’t completely understand what’s going on, but (aside from the annoyance of having to add : Set annotations everywhere) it seems universe polymorphism doesn’t play well with impredicative-set. For instance, the universe-polymorphic funext axiom

funext : forall {A : Type} {P : A -> Type} (f g : forall x : A, P x) (forall x, f x = g x) -> (f = g)

(I’m simplifying a bit from how it’s actually defined) is parametrized by three universes: one for A to belong to (the first occurrence of Type above), one for P to belong to (the second occurrence of Type above), and a third one for forall x : A, P x to belong to, which has to be at least as big as both of the first two. If we then try to instantiate this with A := Set : Type, so the first universe is strictly bigger than Set, while P : Set -> Set, so that the second universe is equal to Set, the constraint that the third universe has to be at least as big as both of the first two universes doesn’t go away, even though under impredicative-set, in this particular instance the third universe doesn’t actually have to be as large as the first one. In other words, the universe polymorphism algorithm doesn’t notice that instantiating particular universes to Set can remove universe constraints.

Possibly I could work around this by asserting a separate funext axiom for Set-valued type families. I haven’t tried, but it seems likely that I would have to duplicate significant parts of Types/Forall.v, which seems tedious and boring.

By the way, universe polymorphism also doesn’t seem to play perfectly well with type-in-type: I still get universe inconsistencies. Seems like I should never get any universe inconsistencies under type-in-type! I haven’t tracked down the cause of this in any more detail, though; putting some things in Set explicitly seems to work around the problem.

• Matt Oliveri says:

Whoops. Forgot this site only has HTML formatting.

For instance, the universe-polymorphic funext axiom … is parametrized by three universes: one for A to belong to (the first occurrence of Type above), one for P to belong to (the second occurrence of Type above), and a third one for forall x : A, P x to belong to, which has to be at least as big as both of the first two.

That already sounds odd. I’m no expert in Coq universe polymorphism, but semantically, I don’t see a need to parameterize by the universe of forall x : A, P x, since the minimal one can be computed. This computation ought to take into account whether the formation rule is impredicative. But I take it that you tried it, and something went wrong, for some reason.

Prior to universe polymorphism, I thought the universe inference algorithm only generated a universe level variable when you literally uttered Type.

• Mike Shulman says:

I’m no expert in the theory of universe polymorphism, but my understanding is that Coq’s universes don’t actually include a “max” operation, so wherever you want to say “max(i,j)” you actually have to give an arbitrary k and assert that i <= k and j <= k.

In fact (repeat caveats about non-expertise) it seems to me that there are at least some reasons to want this behavior: I think it "makes cumulativity admissible" in some sense. That is, if forall x:A, P x is only asserted to live in the max of the universes of A and P, then to make it also live in larger universes one would need an explicit cumulativity rule. But if by definition it lives in any universe larger than those of A and P, then you don’t need an explicit cumulativity rule.

6. Steve Awodey says:

Mike, have you formalized any of this?

• Mike Shulman says:

I’ve formalized the construction of coproducts in Coq, but it’s a bit messy and ad hoc so I haven’t pushed it to the library yet. (I wanted to have at least one case formalized before posting to the blog!) The path algebra gets pretty messy for the cases of higher inductive types; I have some ideas about how to make it more manageable, but haven’t had time to implement them yet.


text:
I wish more of these at least had a reason for why they are blocked.

Oh, it actually looks reasonable. Nice!

Achievement unlocked: use the censor function from MonadWriter in a real piece of code.

This code might require a bit of documentation, though. I am already starting to forget what it is doing.

It's taking the police a while to arrest hundreds of people still on the road.

It's beautiful weather here in The Hague. A perfect day to tell everyone we have to end subsidies for fossil industry.

Google maps has a weird definition of "moderate hill" here in the Netherlands..

From the Delft PL group chat.

Climate

This recently updated post on OWID also seems relevant to the discussion a few days back with @MartinEscardo : ourworldindata.org/environment

format: plain


text:
# Questions tagged as ['xor']

XOR, often written ⊕, is one of the basic operations on bits and bit-sequences. It is a building block of many cryptographic primitives (and some higher-level algorithms, like modes of operations).
Score: 4
Is there any result which states that if the output of these two functions is XOR'd, the XOR'd output is pseudorandom

Let $$\mathbb{G}$$ be a group of prime order $$p$$ with generator $$g$$. Suppose that I randomly pick $$r_1,z_1 \leftarrow \mathbb{Z}_p$$ and $$r_2, z_2 \leftarrow \mathbb{Z}_p$$ and $$c \leftarrow \mathbb{G}$$. Let $$\alpha = g^{r_1z_1}g^{c}$$ and $$\beta = g^{r_2z_2}g^c$$. By the semantic security of El-Gamal encryption, both $$\alpha$$ and $$\beta$$ are indistinguishable from random numbers ... Suppose that $$\alpha$$

Score: 0
What happens when we hash already hashed values, concatenated together?

I read on the page 16 of On the Security of Hash Function Combiners that

the classical combiner for collision-resistance simply concatenates the outputs of both hash functions $$Comb_{\mathbin\|}(M) = H_0(M) \mathbin\| H_1(M)$$ in order to ensure collision resistance as long as either of H0, H1 obeys the property.

Consider H, a secure internal hash function with 256-bit inputs and 128-bit outputs

...
Score: 1
How to show the PRF in 4.8(b) is not secure?

Let F be a PRF defined over $$F:\{0, 1\}^n \times \{0, 1\}^n \to Y$$.

1. We say that $$F$$ is XOR-malleable if $$F(k, x \oplus c) = F(k, x) \oplus c$$ for all $$k, x, c \in \{0, 1\}^n$$.

2. We say that $$F$$ is key XOR-malleable if $$F(k \oplus c, x) = F(k, x) \oplus c$$ for all $$k, x, c \in \{0, 1\}^n$$.

Clearly an XOR-malleable PRF cannot be secure: malleability lets an attacker distinguish the PRF from a random fun ...

Score: 0
Is it possible to crack cryptographic method with known input/output?

I've played around with John The Ripper before and it was able to successfully crack some personal passwords via brute force. However, in those scenarios the "unknown variable" was a password - and the known variable was the encryption method.

In the current scenario, things are a bit different. Now I have a scenario where the 2 input keys are known - and an external tool exists that can convert  ...

Score: 3
Fastest order-sensitive operations

For any $$v$$ many $$b$$-bits vectors $$(\mathbf{x}_0, \mathbf{x}_1, \ldots, \mathbf{x}_{v-1}) \in \{\{0, 1\}^b\}^v$$, what's the fastest way to combine $$\mathbf{x}_0, \mathbf{x}_1, \ldots, \mathbf{x}_{v-1}$$ into a single number, such that the operation is order-sensitive?

E.g. say that $$\hat+$$ is some method of combining numbers (not necessarily addition, but we can define it however we want). The goal is to ...

Score: 1
Is XORing a Base64-encoded string secure?

Theoretically, is it secure to first encode a string using Base64 and then XOR it with a random key or are there potential weaknesses that could be exploited?

Obviously this doesn't make any sense in practice, but I was curious whether this would be just as secure as XORing and then Base64ing.

Score: 4
Weakness of XORing random bytes with secret key

Side A generates 16 (high quality) random bytes and performs XOR with a 16-byte secret key, then data transfers to side B, where the same secret key is used to recover the original 16 random bytes.

Is there, by chance, a way to guess the secret key by intercepting the XORed data between sides?


text:
# The complex number z which satisfies the condition

Question:

The complex number $z$ which satisfies the condition $\left|\frac{i+z}{i-z}\right|=1$ lies on

(a) circle x2 + y2 = 1

(b) the x−axis

(c) the y−axis

(d) the line x + y = 1

Solution:

$\left|\frac{i+z}{i-z}\right|=1$

$\Rightarrow\left|\frac{i+z}{i-z}\right|^{2}=1^{2}$

$\Rightarrow\left(\frac{i+z}{i-z}\right) \overline{\left(\frac{i+z}{i-z}\right)}=1$

$\Rightarrow\left(\frac{i+z}{i-z}\right)\left(\frac{-i+\bar{z}}{-i-\bar{z}}\right)=1$

$\Rightarrow\left(\frac{-i^{2}-z i+\bar{z} i+z \bar{z}}{-i^{2}+z i-\bar{z} i+z \bar{z}}\right)=1$

$\Rightarrow-i^{2}-z i+\bar{z} i+z \bar{z}=-i^{2}+z i-\bar{z} i+z \bar{z}$

$\Rightarrow-z i+\bar{z} i=z i-\bar{z} i$

$\Rightarrow \bar{z} i+\bar{z} i=z i+z i$

$\Rightarrow 2 \bar{z} i=2 z i$

$\Rightarrow \bar{z}=z$

$\Rightarrow z$ is purely real

Hence, the correct option is (b).


text:
# How do you write the equation in slope intercept form given x-3y=6?

Apr 8, 2017

$y = \frac{1}{3} x - 2$

#### Explanation:

Given: $x - 3 y = 6$

Put in slope-intercept form $y = m x + b$:

Add $3 y$ to both sides of the equation to make it positive:

$x - 3 y + 3 y = 6 + 3 y$
$x = 6 + 3 y$

Subtract $6$ from both sides of the equation:

$x - 6 = 6 - 6 + 3 y$
$x - 6 = 3 y$

Divide both sides of the equation by $3$:

$\frac{x}{3} - \frac{6}{3} = \frac{3 y}{3}$
$\frac{1}{3} x - 2 = y$

So $y = \frac{1}{3} x - 2$


text:
The theoretical best basis is usually known for a simulated problem. Augment this information into the data object allows for evaluating the performance of optimisation against the theory.

bind_theoretical(dt, matrix, index, raw_data)

## Arguments

dt a data object collected by the projection pursuit guided tour optimisation in the tourr package a matrix of the theoretical basis the index function used to calculate the index value a tibble of the original data used to calculate the index value

## Value

a tibble object containing both the searched and theoretical best bases

Other bind: bind_random_matrix(), bind_random()
best <- matrix(c(0, 1, 0, 0, 0), nrow = 5)
#> 1 <dbl[,1] [5 × 1]>     0.931 theoretical NA        NA    NA    NA     0


text:
CoCalc
Sharedsupport / 2017-02-15-153823-ideal.sagewsOpen in CoCalc

Examples for support purposes...

P.<x,y,z> = PolynomialRing(RR, 3, order='lex'); P
I = ideal(x^2+y^2+z^2-1, x^2-y+z^2, x-z); I
B = I.groebner_basis(); B

Multivariate Polynomial Ring in x, y, z over Real Field with 53 bits of precision Ideal (x^2 + y^2 + z^2 - 1.00000000000000, x^2 - y + z^2, x - z) of Multivariate Polynomial Ring in x, y, z over Real Field with 53 bits of precision
Error in lines 3-3 Traceback (most recent call last): File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/smc_sagews/sage_server.py", line 982, in execute exec compile(block+'\n', '', 'single') in namespace, locals File "", line 1, in <module> File "sage/misc/cachefunc.pyx", line 2038, in sage.misc.cachefunc.CachedMethodCaller.__call__ (/projects/sage/sage-7.5/src/build/cythonized/sage/misc/cachefunc.c:10792) w = self._instance_call(*args, **kwds) File "sage/misc/cachefunc.pyx", line 1914, in sage.misc.cachefunc.CachedMethodCaller._instance_call (/projects/sage/sage-7.5/src/build/cythonized/sage/misc/cachefunc.c:10238) return self.f(self._instance, *args, **kwds) File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/sage/rings/polynomial/multi_polynomial_ideal.py", line 3731, in groebner_basis gb = self._groebner_basis_singular("groebner", deg_bound=deg_bound, mult_bound=mult_bound, *args, **kwds) File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/sage/interfaces/singular.py", line 2724, in wrapper return func(*args, **kwds) File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/sage/rings/polynomial/multi_polynomial_ideal.py", line 1366, in _groebner_basis_singular S = PolynomialSequence([R(S[i+1]) for i in range(len(S))], R, immutable=True) File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/sage/rings/polynomial/multi_polynomial_ring.py", line 481, in __call__ return x.sage_poly(self) File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/sage/interfaces/singular.py", line 1776, in sage_poly exp[var_dict[var]]=power KeyError: '(1.000e+00)'
P.<x,y,z> = PolynomialRing(RDF, 3, order='lex'); P
I = ideal(x^2+y^2+z^2-1, x^2-y+z^2, x-z); I
B = I.groebner_basis(); B

Multivariate Polynomial Ring in x, y, z over Real Double Field Ideal (x^2 + y^2 + z^2 - 1.0, x^2 - y + z^2, x - z) of Multivariate Polynomial Ring in x, y, z over Real Double Field
Error in lines 3-3 Traceback (most recent call last): File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/smc_sagews/sage_server.py", line 982, in execute exec compile(block+'\n', '', 'single') in namespace, locals File "", line 1, in <module> File "sage/misc/cachefunc.pyx", line 2038, in sage.misc.cachefunc.CachedMethodCaller.__call__ (/projects/sage/sage-7.5/src/build/cythonized/sage/misc/cachefunc.c:10792) w = self._instance_call(*args, **kwds) File "sage/misc/cachefunc.pyx", line 1914, in sage.misc.cachefunc.CachedMethodCaller._instance_call (/projects/sage/sage-7.5/src/build/cythonized/sage/misc/cachefunc.c:10238) return self.f(self._instance, *args, **kwds) File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/sage/rings/polynomial/multi_polynomial_ideal.py", line 3731, in groebner_basis gb = self._groebner_basis_singular("groebner", deg_bound=deg_bound, mult_bound=mult_bound, *args, **kwds) File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/sage/interfaces/singular.py", line 2724, in wrapper return func(*args, **kwds) File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/sage/rings/polynomial/multi_polynomial_ideal.py", line 1366, in _groebner_basis_singular S = PolynomialSequence([R(S[i+1]) for i in range(len(S))], R, immutable=True) File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/sage/rings/polynomial/multi_polynomial_ring.py", line 481, in __call__ return x.sage_poly(self) File "/projects/sage/sage-7.5/local/lib/python2.7/site-packages/sage/interfaces/singular.py", line 1776, in sage_poly exp[var_dict[var]]=power KeyError: '(1.000e+00)'


text:
# Beamer template problem: flushright frame subtitle causes spurious extra slide (or worse!)

So here is a MWE that illustrates the problem.

\documentclass{beamer}
\defbeamertemplate{frametitle}{weird}{%
\insertframetitle\par%
\rule{\textwidth}{4pt}%
\flushright%
\insertframesubtitle\par%
}
\setbeamertemplate{frametitle}[weird]
\begin{document}
\begin{frame}
\frametitle{Here is the title}
%\framesubtitle{Here is the subtitle}
Here is the text
\pause
Here is more text
\end{frame}
\end{document}

This code fails with a:

! LaTeX Error: Something's wrong--perhaps a missing \item.

Commenting out the \pause or \flushright or uncommenting the \framesubtitle allows it to compile. [Commenting out the \pause leads to a spurious empty page at the end.]

So my guess is that this is a "wrong mode" problem when the subtitle is empty. But I don't know enough to fix it. Any clues? Or any hints on what to try in order to fix it?

-

where is the sense to use the two macros instead of using the arguments of frame? This works:

\begin{frame}{Here is the title}{Here is the subtitle}

you should also check for an existing subtitle:

\documentclass{beamer}
\makeatletter
\defbeamertemplate{frametitle}{weird}{%
\insertframetitle\par%
\rule{\textwidth}{4pt}%
\ifx\insertframesubtitle\@empty\else
\flushright%
\insertframesubtitle\par\fi}
\makeatother
\setbeamertemplate{frametitle}[weird]
\begin{document}
\begin{frame}{Here is the title}{}
Here is the text
\pause
Here is more text
\end{frame}
\end{document}

-
\begin{frame}{Title}{} breaks. –  Seamus Oct 11 '11 at 11:51
So does \begin{frame}{Title} (i.e. just the one extra argument. As for why use these macros? I read somewhere they are more robust, and I think they're more semantic. [Also, emacs does them automatically...] –  Seamus Oct 11 '11 at 11:53
see edit for handling a missing subtitle –  Herbert Oct 11 '11 at 11:58
Thanks! So it is a problem with TeX not liking to \flushright an empty paragraph, right? Why is this? –  Seamus Oct 11 '11 at 12:25
I suppose a problem with horizontal and vertical mode, but I am not really sure. The code of beamer is not really user friendly ... –  Herbert Nov 2 '11 at 16:41


text: 0 1. It can be said that these parallel rays will converge at infinity. parallel to the focal axis), it is reflected back by 180* parallel to the focal axis. The enlarged image is located 5.6 cm behind the mirror. Solution: The radius of curvature of the mirror = 30 cm Thus, the focal length of the mirror =$$\frac { 30 cm }{ 2 }$$ = 15 cm. What is the focal length of a plane mirror? Solution: We have u = … When a photographic lens is set to "infinity", its rear nodal point is separated from the sensor or film, at the focal plane, by the lens's focal length… The focal length of a plane mirror is infinity as the image can be formed at an infinite distance inside the mirror. 23 hours ago. Focal length of a plane mirror is infinite. Focal length is half of radius of curvature and hence it is infinity. (b) Determine the focal length of the mirror. Two plane mirrors are located parallel to each other and are separated by 90.0 cm as shown in figure 1. You can use the mirror formula also to get the focal length of a plane mirror, where the image distance = − object distance. 20 hours ago, Posted A dentistA??? Find the position of the image. 19 hours ago, Posted Calculate this using the spherical mirror equation and the fact that do-di 2. For a standard rectilinear lens, FOV = 2 arctan x / 2f, where x is the diagonal of the film. …. ?1s mirror is placed 2.0 cm from a tooth. 13 hours ago, Posted (a) What is the focal length of a plane mirror? Add your answer and earn points. 6 years ago, Posted When a photographic lens is set to "infinity", its rear nodal point is separated from the sensor or film, at the focal plane, by the lens's focal length… 1/F = 1/U - 1/U = 0. A plane mirror is considered as the limit of either a concave or a convex spherical curved mirror as the radius & so the focal length becomes infinite. 0 0. What is themagnification of a plane mirror? 1. The enlarged image is located 5.6 cm behind the mirror. ius of the hole if both of the spirit and the plate are kept at the same temperature how much heat must be put into the two so that the ball just passes through the hole. The focal length of a plane mirror is infinity as the image can be formed at an infinite distance inside the mirror. Get … one year ago, Posted Anonymous. That is F = infinity. samriddhiyadav717 is waiting for your help. yesterday, Posted In a plane mirror, the radius of curvature is infinitly long, so the focus will be at infinity. Best Answer 100% (1 rating) Previous question Next question Get more help from Chegg. Focal length (f) and field of view (FOV) of a lens are inversely proportional. You can specify conditions of storing and accessing cookies in your browser. Example 4: An object is placed at a distance of 15 cm from a concave mirror of focal length 10 cm. (a) What kind of mirror (plane, concave, or convex) is being used? Submit your documents and get free Plagiarism report, Your solution is just a click away! (b) Determine the focal length of the mirror. For a standard rectilinear lens, FOV = 2 arctan x / 2f, where x is the diagonal of the film. In a plane mirror, the radius of curvature is infinitly long, so the focus will be at infinity. 1 decade ago. There is no focal length for a plane mirrior!!!! Pinky A. (a) What kind of mirror (plane, concave, or convex) is being used? © 2007-2020 Transweb Global Inc. All rights reserved. What is the magnification of a plane mirror? What is the focal length of a plane mirror? Log into your existing Transtutors account. Solution: We have u = –15 cm and f = –10 cm Posted 16 hours ago, Posted ?1s mirror is placed 2.0 cm from a tooth. Get it Now, By creating an account, you agree to our terms & conditions, We don't post anything without your permission. !, because there is no centre of curvature. Example 4: An object is placed at a distance of 15 cm from a concave mirror of focal length 10 cm. Get it solved from our top experts within 48hrs! I know that the focal lengthof a plane mirror is infinite, but I need help with themagnification. Source(s): My sources are my science textbooks!!!!!. Focal length (f) and field of view (FOV) of a lens are inversely proportional. What is the focal length of the plane mirror?, explain yy a magnetic material is attached by a magnet, Establish relation between elements of earth's magnetic field., Join kro sabhiI'd-934 723 6482pass-1234join me,, PLEASE ANSWER WITH FULL SOLUTIONPLEASE DON'T SPAM, A 1.94 kg steel sphere will not fit through a circular hole im a 0.671 kg aluminum plate, because the radius of the spear is 0.10% larger than the rad A dentistA??? Solution: The radius of curvature of the mirror = 30 cm Thus, the focal length of the mirror =$$\frac { 30 cm }{ 2 }$$ = 15 cm. When an object is placed infront of a plane-mirror an image is formed behind the mirror at a distance equal to the distance of the object from the mirror.That is distance of the image from the mirror= V = -U. from the law of distances, 1/F = 1/U + 1/V. 4 years ago, Posted This site is using cookies under cookie policy. A plane mirror can be considered as a spherical mirror of infinite radius of curvature. This can be shown as follows... when a ray of light falls on the mirror perpendicularly (i.e. Find the position of the image. No focal length in plane mirror,because there is no center of curvature in plane mirror.


text:
# Influence line diagram for BM at P for cantilever as shown is:

This question was previously asked in
MPSC AE CE Mains 2019 Official (Paper 1)
View all MPSC AE Papers >

Option 1 :
Free
CT 1: Ratio and Proportion
1963
10 Questions 16 Marks 30 Mins

## Detailed Solution

Explanation:

For Influence line diagram for Bending moment at p, give at hinge at point p, so that it rotate by angle θ when unit load at point B = -1 × C = - C

When unit load is at p, bending moment at A = 0

So ILD for B mat p ⇒ $$\tan \theta \simeq {\theta _p} = \frac{C}{C} = 1\;$$


text:
Public Group

# I "Confused" My Compiler!?

This topic is 4487 days old which is more than the 365 day threshold we allow for new replies. Please post a new topic.

## Recommended Posts

Wow. :| Well I'm sure this has to do with strings and pointers. I probably tried to print by address or something wrong. Anyway...get this error: "/stddef.h:153: confused by earlier errors, bailing out" My compiler bailed on me! :D Seriously though, this is strange. It told me all the errors are in stddef.h. What could I have possibly done that would've caused that?

##### Share on other sites
Care to list the other errors? If it tells you that there are so many errors, it can't even look for any more, maybe you should worry about those. If the error is in seperate file, there are a couple things that could have happened. Check before you include the file for any missing semicolons or other syntax errors. Also, are you sure you didn't accidentally change anything with the file?

##### Share on other sites
Quote:
 Original post by Sr_GuapoCare to list the other errors? If it tells you that there are so many errors, it can't even look for any more, maybe you should worry about those. If the error is in seperate file, there are a couple things that could have happened. Check before you include the file for any missing semicolons or other syntax errors. Also, are you sure you didn't accidentally change anything with the file?

Yeah sure...here's the complete listing:

[SOURCE]C:\Documents and Settings\(MY NAME)\My Documents\Assignment 6>g++ -c PrintData.cppIn file included from PrintData.cpp:1:stocks.h:47:7: warning: no newline at end of fileIn file included from C:/Documents and Settings/(MY NAME)/My Documents/School/(MY SCHOOL)/11th Grade/Quarter 2/Intro to C/MinGW/include/c++/3.2.3/iosfwd:45,                 from C:/Documents and Settings/(MY NAME)/My Documents/School/(MY SCHOOL)/11th Grade/Quarter 2/Intro to C/MinGW/include/c++/3.2.3/ios:44,                 from C:/Documents and Settings/(MY NAME)/My Documents/School/(MY SCHOOL)/11th Grade/Quarter 2/Intro to C/MinGW/include/c++/3.2.3/ostream:45,                 from C:/Documents and Settings/(MY NAME)/My Documents/School/(MY SCHOOL)/11th Grade/Quarter 2/Intro to C/MinGW/include/c++/3.2.3/iostream:45,                 from PrintData.cpp:2:C:/Documents and Settings/(MY NAME)/My Documents/School/(MY SCHOOL)/11th Grade/Quarter 2/Intro to C/MinGW/include/c++/3.2.3/bits/stringfwd.h: In   function char* GetMonth(int)':C:/Documents and Settings/(MY NAME)/My Documents/School/(MY SCHOOL)/11th Grade/Quarter 2/Intro to C/MinGW/include/c++/3.2.3/bits/stringfwd.h:46: parse   error before namespace'C:/Documents and Settings/(MY NAME)/My Documents/School/(MY SCHOOL)/11th Grade/Quarter 2/Intro to C/MinGW/include/c++/3.2.3/bits/stringfwd.h:54: parse   error before <' tokenC:/Documents and Settings/(MY NAME)/My Documents/School/(MY SCHOOL)/11th Grade/Quarter 2/Intro to C/MinGW/include/c++/3.2.3/bits/stringfwd.h:58: explicit   specialization in non-namespace scope char* GetMonth(int)'C:/Documents and Settings/(MY NAME)/My Documents/School/(MY SCHOOL)/11th Grade/Quarter 2/Intro to C/MinGW/include/c++/3.2.3/bits/stringfwd.h:58:    char_traits' is not a templateC:/Documents and Settings/(MY NAME)/My Documents/School/(MY SCHOOL)/11th Grade/Quarter 2/Intro to C/MinGW/include/c++/3.2.3/bits/stringfwd.h:60: syntax   error before ;' tokenC:/Documents and Settings/(MY NAME)/My Documents/School/(MY SCHOOL)/11th Grade/Quarter 2/Intro to C/MinGW/lib/gcc-lib/mingw32/3.2.3/include/stddef.h:153: confused by earlier errors, bailing out[/SOURCE]

##### Share on other sites
Maybe if you could post your code, it may make a bit more sense. It looks like this is a homework assignment, so we can't really just tell you the answer, but we can definately help point you in the correct direction!

##### Share on other sites
Try posting where you include cstddef (or whatever includes it) and the code right before it.

##### Share on other sites
Quote:
 Original post by Sr_GuapoMaybe if you could post your code, it may make a bit more sense. It looks like this is a homework assignment, so we can't really just tell you the answer, but we can definately help point you in the correct direction!

Ah don't worry. It was a homework assignment, but I gave up on it because my approach was way off. (it's only like 1% of my grade and it's due tommorow, the last day of class, anyway)

But sure..you can look at the code. Like I said though, I'm pretty sure it's a string problem. My teacher never taught us to use C++ strings, just character arrays.

[SOURCE]#include "stocks.h"#include <iostream>void PrintData(struct stock &x){	int i = 0;	for(;;)	{		cout << "                                " // CENTERING			 << x.symbol << ':' << GetYear(i);		for(;;)		{			if( (i-1)%372 = 0) break;		    cout << "\n" << GetMonth(i) 			     << "        "				 << "*-----Open----* *-----High----*"				 << "*----Low ----* *----Close----* "				 << "          "				 << "Max     Min     Max     Min"				 << "     Max    Min     Max     Min"				 << endl;					}		}}int GetYear(int i) { if(i < 372) return 2004; else return 2005;}char * GetMonth(int i){	float j = (i-1)/31;	if(j < 1) return "Jan.";	if(j < 2) return "Feb.";	if(j < 3) return "Mar.";	if(j < 4) return "Apr.";	if(j < 5) return "May.";	if(j < 6) return "Jun.";	if(j < 7) return "Jul.";	if(j < 8) return "Aug.";	if(j < 9) return "Sep.";	if(j < 10)return "Oct.";	if(j < 11)return "Nov.";	if(j < 12)return "Dec.";	if(j < 13)return "Jan.";	if(j < 14)return "Feb.";	if(j < 15)return "Mar.";	if(j < 16)return "Apr.";	if(j < 17)return "May.";	if(j < 18)return "Jun.";	if(j < 19)return "Jul.";	if(j < 20)return "Aug.";	if(j < 21)return "Sep.";	if(j < 22)return "Oct.";	if(j < 23)return "Nov.";	else      return "Dec.";}[/SOURCE]

##### Share on other sites
EDIT: Nevermind.

That's some ugly code. The use of char* for strings in C++ is, as you mentioned, particularly nasty. The most obvious think I see is that you need to qualify objects in the std namespace (std::cout) or insert a "using std::cout" or "using namespace std" near the top someplace. Unless stocks.h has it... but that would be evil as well.

Use std::string unless your teacher/professor has explicitly forbid it (or explicitly required char*... in which case change the return type of GetMonth() to const char* at least).

##### Share on other sites
Quote:
 Original post by CTarTry posting where you include cstddef (or whatever includes it) and the code right before it.

But i don't. :| I just included iostream and my own header file.

##### Share on other sites
For a start - put some newlines at the end of your "stocks.h" file.
Unlike Visual C++, gcc has some problems if there is no newline symbols at the end of included header file (had some problems with this issue myself).

EDIT: you don't have any 'using' statements, but you use cout and endl as if they are not in std namespace - either you didn't post all code, or you missed it.

1. 1
2. 2
Rutin
21
3. 3
4. 4
frob
17
5. 5

• 9
• 12
• 9
• 33
• 13
• ### Forum Statistics

• Total Topics
632594
• Total Posts
3007259

×

## Important Information

We are the game development community.

Whether you are an indie, hobbyist, AAA developer, or just trying to learn, GameDev.net is the place for you to learn, share, and connect with the games industry. Learn more About Us or sign up!

Sign me up!


text:
unit:UnitPole

Type
Description

A magnetic pole is a unit pole if it exerts a force of one dyne on another pole of equal strength at a distance of 1 cm. The strength of any given pole in cgs units is therefore numerically equal to the force in dynes which it exerts on a unit pole 1 cm away.

Properties
0.0000001256637
0112/2///62720#UAB214
Annotations
A magnetic pole is a unit pole if it exerts a force of one dyne on another pole of equal strength at a distance of 1 cm. The strength of any given pole in cgs units is therefore numerically equal to the force in dynes which it exerts on a unit pole 1 cm away.
$$U/nWb$$
Unit Pole(en)

Generated 2021-09-16T15:58:01.983-07:00 by lmdoc version 1.1 with  TopBraid SPARQL Web Pages (SWP)


text:
# Help Sawmill application: Voltage drop.

## Main Question or Discussion Point

Before I go too indepth, I wanted to make sure this was the proper place to post this. I stated in my intro I am doing a co-op work experience. I am working at a sawmill, and I have been asked to look at a few situations and things like that around the mill. I have been here for a couple weeks and the one situation they gave me I am fairly confused about.

This mill is 3 phase, 120/208 VAC supply. My use of terms may be wrong, as I am still getting used to everything. I can draw... or attempt to draw the circuits my supervisor gave me, but basically there is a problem with the voltage.

The 120V supply goes to the one machine, and then right after the machine it is grounded and there are neutral wires as well which the current should flow through. However, instead of that happening, there was 6.7V on the ground end of the load/machine. So to fix this temporarily, there was a jumper put in place from the neutral wire to the machine ground. I am to figure out what is going on and why there is that 6.7V after the load/machine and fix it so the jumper can be taken out of place.

Related Electrical Engineering News on Phys.org
berkeman
Mentor
As I mentioned in your intro post, I'm not much help on 3-phase power systems. But there are plenty of other folks here who are, so they should chime in at some point.

For now, here's an intro from wikipedia.org -- you may already know all of this stuff in the basic intro, though.

http://en.wikipedia.org/wiki/Three-phase_power

NoTime
Homework Helper
The 120V supply goes to the one machine, and then right after the machine it is grounded and there are neutral wires as well which the current should flow through. However, instead of that happening, there was 6.7V on the ground end of the load/machine. So to fix this temporarily, there was a jumper put in place from the neutral wire to the machine ground. I am to figure out what is going on and why there is that 6.7V after the load/machine and fix it so the jumper can be taken out of place.
First, the existing "solution" is dangerous.
The thing should be tagged out of service until a proper repair is made.
That is assuming that the issue only affects this one unit.

That said.
The 120v supply indicates, to me anyway, that this particular unit is a single phase motor.
Three wires hot, neutral and ground.
Not that phase count makes a real difference if the problem is with the ground plane.

How was it determined that the ground was at fault rather than the neutral?
Voltage on the ground wire (not a good thing) implies that the connecting cable is damaged or a bad connection at a junction box or panel.

Not sure why the current "solution" to this is being used. This is one of the top priorities at the moment because this 'jumper' is unsafe. Well, right now, not totally sure if it's a problem with the ground wiring, or the neutral wiring. The return (both the ground & neutral I believe) is something like 600 feet of 4/0 wire. Now, if there's bad connections, or burned out busses, that could add resistance, but without that, the resistance for 600 feet of 4/0 wire is only 0.0294 ohms... I think. Very small anyways.

NoTime
Homework Helper
What's the horsepower on the motor?
How exactly is it connected. single, delta or wye?

To find out if the neutral or ground is bad.
Since there should be very little current on the ground (perhaps some leakage) you could try to measure the resistance to a known good ground point (with the motor off).
Or could run a temporary ground to a known good ground point for this circuit.

Particularly if it's Al wire, you could have an oxidized connection.
You might need to remake the connections using a fresh coat of the proper Al grease.

turbo
Gold Member
In older installations, 3-phase motors could often continue to run with one leg of the 3 phases in ground-fault, and only fail to operate when a second leg faults. You should specify if your mill is wired delta or wye.

dlgoff
Gold Member
There is the posibility that the motor is causing the problem. Maybe there is leakage from the windings to your ground.

I'll ask and find out about delta or wye, along with the horsepower of the motor/machine. The mill is new and has only been in operation for a year and a half too though.

turbo
Gold Member
Err, if you are tasked with this responsibility and you are not yet aware of the way that the distribution system and motors are wired, you are in dangerous territory. Get some help, or you could kill yourself or some other employee unlucky enough to contact a couple of pieces of equipment or grounded infrastructure (maybe rub up against a motor housing while standing on concrete). You or a fellow employee may become a conductor across a high enough voltage potential to kill at the amperage levels that this commercial supply can provide. Don't ask for help here. Get expert help, and learn from that expert. It could save lives.

I do have help, and I have electricians taking measurements. I am a student... learning. That's why I am in this environment with this task. I am unfamiliar, therefore I don't touch. My supervisor is helping me with this, but he is trying to figure it out. As for me, since I am going into electrical engineering, and he is a supervisor, I know some theoretical and practical applications he may not, and he knows a lot more than me though.

Averagesupernova
Gold Member
The 120V supply goes to the one machine, and then right after the machine it is grounded and there are neutral wires as well which the current should flow through. However, instead of that happening, there was 6.7V on the ground end of the load/machine. So to fix this temporarily, there was a jumper put in place from the neutral wire to the machine ground. I am to figure out what is going on and why there is that 6.7V after the load/machine and fix it so the jumper can be taken out of place.
Am I to assume that there is 6.7 volts between the frame of the machine (conduit ground) and the neutral wire? You don't really specifically say, but I would assume. The neutral and ground should NEVER be connected together except at the main service panel. Any panel, disconnect, sub-panel, etc. after the main panel should keep these 2 conductors isolated. If there is a voltage build up between neutral and ground then you need to start at the FAR end of the line (machine) and start disconnecting things. Is the voltage present all the time or just when the machine is running and drawing current? From the little that I've learned so far I'd say there is a poor connection on the neutral wire somewhere upstream.

This is how the circuit was drawn for me by my supervisor,

Code:
 |-----------------------------------------------------|
|                                                   A |
|                                                     |
Vs                                                     L
|                                                     |
|                                                   B |---J---|
|                                                     |       |
|-----------------------------------------------------|       |
|                                                             |
|-------------------------------------------------------------|
|
GND
Vs is the source power, 120 volt supply. "L" is the load which requires this power and the next figure shows the connections a little more clearly. Now apparently between "A" and "B" there is 113.3V. "J" is the jumper and connected directly to the body of the machine, and is temporarily in place to lower that 6.7V.

The setup for the machine/load itself looks like this... which when my supervisor gave to me confused me for a few minutes because I had to understand it as well.

Code:
               |----------------------|
| Optimizer End Column |
|--------------|                      |
|              |                      |
|   A|--N      |                      |
|    |         |                      |
|----O---------|                      |
|                      |
|                      |
|                      |
|------O                      |
|      |----------------------|
B |
|
|             16.7A @ 60.0 Hz               To PDC
<-------O----------------------------------------------->
"N" is where the neutral wire is, and the lead coming off from that "A" connects to the machine itself (bolted). "N" also is where the ground and power (from the first diagram) are located. "A" in this diagram is the jumper from the first diagram, and has 5.7A across it, and "B" has 4.2A across it which is the machine ground. This machine ground connects to the main mill ground which has 16.7A @ 60Hz and goes to the PDC.

Now yesterday, I asked my supervisor before he ran off but he said there are also 2 other connections to the machine that are connected to ground for other instrumentation purposes. I believe this may make up for the 1.5A lost from cable A to cable B. An electrician said there will be more data later today if he gets around to it from the cables attached and related to this as well.

I believe there may be poor connections or corrosion, I just wanted some input or advice from others because of their experience.

Averagesupernova
Gold Member
Your previous post doesn't make alot of sense to me. It sounds to me like you are mixing up voltage and current since you are referring to something that has current 'across' it. Current is a rate of electrons passing a given point in a given amount of time. It is never 'across' anything. Also, as far as I can tell there are several places where there are currents flowing on a ground wire. Ground wires are NEVER meant to carry current except in a fault condition.

Ya, it's a new mill with some serious problems like this. I meant to say current flowing through... but those are both currents and not voltages. I recently just finished 2nd year of my program, and been working here for 2 weeks, and I recently was asked to help my supervisor with this situation. I understand that in an application like this, the ground shouldn't have any current, only the neutral...

stewartcs
I presume you actually have 120 VAC being supplied from the source and not 113.3 VAC? If so you'll most likely have an isulation resistance fault. Tell the electrician to "megger" the unit (if possible) and see if there is are any faults.

Hope that helps.

CS

Yes, there is 120 VAC being supplied from the source. My supervisor has asked the electricians to get the numbers from various cables connected to the machine. They are busy, but hopefully I will get some readings soon. Apparently this problem has been there since the mill started up. All the comments are giving me a lot of things to look at which is good. Thanks.

NoTime


text:
### Glossary

• alternate interior angles

Alternate interior angles are created when two parallel lines are crossed by another line called a transversal. Alternate interior angles are inside the parallel lines and on opposite sides of the transversal.

This diagram shows two pairs of alternate interior angles. Angles $$a$$ and $$d$$ are one pair and angles $$b$$ and $$c$$ are another pair.

• base (of an exponent)

In expressions like $$5^3$$ and $$8^2$$, the 5 and the 8 are called bases. They tell you what factor to multiply repeatedly. For example, $$5^3$$ = $$5 \boldcdot 5 \boldcdot 5$$, and $$8^2 = 8 \boldcdot 8$$.

• center of a dilation

The center of a dilation is a fixed point on a plane. It is the starting point from which we measure distances in a dilation.

In this diagram, point $$P$$ is the center of the dilation.

• clockwise

Clockwise means to turn in the same direction as the hands of a clock. The top turns to the right. This diagram shows Figure A turned clockwise to make Figure B.

• coefficient

A coefficient is a number that is multiplied by a variable.

For example, in the expression $$3x+5$$, the coefficient of $$x$$ is 3. In the expression $$y+5$$, the coefficient of $$y$$ is 1, because $$y=1 \boldcdot y$$.

• cone

A cone is a three-dimensional figure like a pyramid, but the base is a circle.

• congruent

One figure is congruent to another if it can be moved with translations, rotations, and reflections to fit exactly over the other.

In the figure, Triangle A is congruent to Triangles B, C, and D. A translation takes Triangle A to Triangle B, a rotation takes Triangle B to Triangle C, and a reflection takes Triangle C to Triangle D.

• constant of proportionality

In a proportional relationship, the values for one quantity are each multiplied by the same number to get the values for the other quantity. This number is called the constant of proportionality.

In this example, the constant of proportionality is 3, because $$2 \boldcdot 3 = 6$$, $$3 \boldcdot 3 = 9$$, and $$5 \boldcdot 3 = 15$$. This means that there are 3 apples for every 1 orange in the fruit salad.

number of oranges number of apples
2 6
3 9
5 15
• constant term

In an expression like $$5x+2$$, the number 2 is called the constant term because it doesn’t change when $$x$$ changes.

In the expression $$7x+9$$, 9 is the constant term.
In the expression $$5x+(\text-8)$$, -8 is the constant term.
In the expression $$12-4x$$, 12 is the constant term.

• coordinate plane

The coordinate plane is a system for telling where points are. For example. point $$R$$ is located at $$(3, 2)$$ on the coordinate plane, because it is three units to the right and two units up.

• corresponding

When part of an original figure matches up with part of a copy, we call them corresponding parts. These could be points, segments, angles, or distances.

For example, point $$B$$ in the first triangle corresponds to point $$E$$ in the second triangle. Segment $$AC$$ corresponds to segment $$DF$$.

• counterclockwise

Counterclockwise means to turn opposite of the way the hands of a clock turn. The top turns to the left.

This diagram shows Figure A turned counterclockwise to make Figure B.

• cube root

The cube root of a number $$n$$ is the number whose cube is $$n$$. It is also the edge length of a cube with a volume of $$n$$. We write the cube root of $$n$$ as $$\sqrt[3]{n}$$.

For example, the cube root of 64, written as $$\sqrt[3]{64}$$, is 4 because $$4^3$$ is 64. $$\sqrt[3]{64}$$ is also the edge length of a cube that has a volume of 64.

• cylinder

A cylinder is a three-dimensional figure like a prism, but with bases that are circles.

• dependent variable

A dependent variable represents the output of a function.

For example, suppose we need to buy 20 pieces of fruit and decide to buy apples and bananas. If we select the number of apples first, the equation $$b=20-a$$ shows the number of bananas we can buy. The number of bananas is the dependent variable because it depends on the number of apples.

• dilation

A dilation is a transformation in which each point on a figure moves along a line and changes its distance from a fixed point. The fixed point is the center of the dilation. All of the original distances are multiplied by the same scale factor.

For example, triangle $$DEF$$ is a dilation of triangle $$ABC$$. The center of dilation is $$O$$ and the scale factor is 3.

This means that every point of triangle $$DEF$$ is 3 times as far from $$O$$ as every corresponding point of triangle $$ABC$$.

• exponent

In expressions like $$5^3$$ and $$8^2$$, the 3 and the 2 are called exponents. They tell you how many factors to multiply. For example, $$5^3$$ = $$5 \boldcdot 5 \boldcdot 5$$, and $$8^2 = 8 \boldcdot 8$$.

• function

A function is a rule that assigns exactly one output to each possible input.

The function $$y=6x+4$$ assigns one value of the output, $$y$$, to each value of the input, $$x$$. For example, when $$x$$ is 5, then $$y=6(5)+4$$ or 34.

• hypotenuse

The hypotenuse is the side of a right triangle that is opposite the right angle. It is the longest side of a right triangle.

Here are some right triangles. Each hypotenuse is labeled.

• image

An image is the result of translations, rotations, and reflections on an object. Every part of the original object moves in the same way to match up with a part of the image.

In this diagram, triangle $$ABC$$ has been translated up and to the right to make triangle $$DEF$$. Triangle $$DEF$$ is the image of the original triangle $$ABC$$.

• independent variable

An independent variable represents the input of a function.

For example, suppose we need to buy 20 pieces of fruit and decide to buy some apples and bananas. If we select the number of apples first, the equation $$b=20-a$$ shows the number of bananas we can buy. The number of apples is the independent variable because we can choose any number for it.

• irrational number

An irrational number is a number that is not a fraction or the opposite of a fraction.

Pi ($$\pi$$) and $$\sqrt2$$ are examples of irrational numbers.

• legs

The legs of a right triangle are the sides that make the right angle.

Here are some right triangles. Each leg is labeled.

• linear relationship

A linear relationship between two quantities means they are related like this: When one quantity changes by a certain amount, the other quantity always changes by a set amount. In a linear relationship, one quantity has a constant rate of change with respect to the other.

The relationship is called linear because its graph is a line.

The graph shows a relationship between number of days and number of pages read.

When the number of days increases by 2, the number of pages read always increases by 60. The rate of change is constant, 30 pages per day, so the relationship is linear.

• negative association

A negative association is a relationship between two quantities where one tends to decrease as the other increases. In a scatter plot, the data points tend to cluster around a line with negative slope.

Different stores across the country sell a book for different prices.

The scatter plot shows that there is a negative association between the the price of the book in dollars and the number of books sold at that price.

• outlier

An outlier is a data value that is far from the other values in the data set.

Here is a scatter plot that shows lengths and widths of 20 different left feet. The foot whose length is 24.5 cm and width is 7.8 cm is an outlier.

• positive association

A positive association is a relationship between two quantities where one tends to increase as the other increases. In a scatter plot, the data points tend to cluster around a line with positive slope.

The relationship between height and weight for 25 dogs is shown in the scatter plot. There is a positive association between dog height and dog weight.

• Pythagorean Theorem

The Pythagorean Theorem describes the relationship between the side lengths of right triangles.

The diagram shows a right triangle with squares built on each side.  If we add the areas of the two small squares, we get the area of the larger square.

The square of the hypotenuse is equal to the sum of the squares of the legs. This is written as $$a^2+b^2=c^2$$.

A radius is a line segment that goes from the center to the edge of a circle. A radius can go in any direction. Every radius of the circle is the same length. We also use the word radius to mean the length of this segment.

For example, $$r$$ is the radius of this circle with center $$O$$.

• rate of change

The rate of change in a linear relationship is the amount $$y$$ changes when $$x$$ increases by 1. The rate of change in a linear relationship is also the slope of its graph.

In this graph, $$y$$ increases by 15 dollars when $$x$$ increases by 1 hour. The rate of change is 15 dollars per hour.

• rational number

A rational number is a fraction or the opposite of a fraction.

Some examples of rational numbers are: $$\frac74,0,\frac63,0.2,\text-\frac13,\text-5,\sqrt9$$

• reciprocal

Dividing 1 by a number gives the reciprocal of that number. For example, the reciprocal of 12 is $$\frac{1}{12}$$, and the reciprocal of $$\frac25$$ is $$\frac52$$.

• reflection

A reflection across a line moves every point on a figure to a point directly on the opposite side of the line. The new point is the same distance from the line as it was in the original figure.

This diagram shows a reflection of A over line $$\ell$$ that makes the mirror image B.

• relative frequency

The relative frequency of a category tells us the proportion at which the category occurs in the data set. It is expressed as a fraction, a decimal, or a percentage of the total number.

For example, suppose there were 21 dogs in the park, some white, some brown, some black, and some multi-color. The table shows the frequency and the relative frequency of each color.

color frequency relative frequency
white 5 $$\frac{5}{21}$$
brown 7 $$\frac{7}{21}$$
black 3 $$\frac{3}{21}$$
multi-color 6 $$\frac{6}{21}$$
• repeating decimal

A repeating decimal has digits that keep going in the same pattern over and over. The repeating digits are marked with a line above them.

For example, the decimal representation for $$\frac13$$ is $$0.\overline{3}$$, which means 0.3333333 . . . The decimal representation for $$\frac{25}{22}$$ is $$1.1\overline{36}$$ which means 1.136363636 . . .

• right angle

A right angle is half of a straight angle. It measures 90 degrees.

• rigid transformation

A rigid transformation is a move that does not change any measurements of a figure. Translations, rotations, and reflections are rigid transformations, as is any sequence of these.

• rotation

A rotation moves every point on a figure around a center by a given angle in a specific direction.

This diagram shows Triangle A rotated around center $$O$$ by 55 degrees clockwise to get Triangle B.

• scale factor

To create a scaled copy, we multiply all the lengths in the original figure by the same number. This number is called the scale factor.

In this example, the scale factor is 1.5, because $$4 \boldcdot (1.5) = 6$$, $$5 \boldcdot (1.5)=7.5$$, and $$6 \boldcdot (1.5)=9$$.

• scatter plot

A scatter plot is a graph that shows the values of two variables on a coordinate plane. It allows us to investigate connections between the two variables.

Each plotted point corresponds to one dog. The coordinates of each point tell us the height and weight of that dog.

• scientific notation

Scientific notation is a way to write very large or very small numbers. We write these numbers by multiplying a number between 1 and 10 by a power of 10.

For example, the number 425,000,000 in scientific notation is $$4.25 \times 10^8$$. The number 0.0000000000783 in scientific notation is $$7.83 \times 10^{\text-11}$$.

• segmented bar graph

A segmented bar graph compares two categories within a data set. The whole bar represents all the data within one category. Then, each bar is separated into parts (segments) that show the percentage of each part in the second category.

This segmented bar graph shows the percentage of people in different age groups that do and do not have a cell phone. For example, among people ages 10 to 12, about 40% have a cell phone and 60% do not have a cell phone.

• sequence of transformations

A sequence of transformations is a set of translations, rotations, reflections, and dilations on a figure. The transformations are performed in a given order.

This diagram shows a sequence of transformations to move Figure A to Figure C.

First, A is translated to the right to make B. Next, B is reflected across line $$\ell$$ to make C.

• similar

Two figures are similar if one can fit exactly over the other after rigid transformations and dilations.

In this figure, triangle $$ABC$$ is similar to triangle $$DEF$$.

If $$ABC$$ is rotated around point $$B$$ and then dilated with center point $$O$$, then it will fit exactly over $$DEF$$. This means that they are similar.

• slope

The slope of a line is a number we can calculate using any two points on the line. To find the slope, divide the vertical distance between the points by the horizontal distance.

The slope of this line is 2 divided by 3 or $$\frac23$$.

• solution to an equation with two variables

A solution to an equation with two variables is a pair of values of the variables that make the equation true.

For example, one possible solution to the equation $$4x+3y=24$$ is $$(6,0)$$. Substituting 6 for $$x$$ and 0 for $$y$$ makes this equation true because $$4(6)+3(0)=24$$.

• sphere

A sphere is a three-dimensional figure in which all cross-sections in every direction are circles.

• square root

The square root of a positive number $$n$$ is the positive number whose square is $$n$$. It is also the the side length of a square whose area is $$n$$. We write the square root of $$n$$ as $$\sqrt{n}$$.

For example, the square root of 16, written as $$\sqrt{16}$$, is 4 because $$4^2$$ is 16.

$$\sqrt{16}$$ is also the side length of a square that has an area of 16.

• straight angle

A straight angle is an angle that forms a straight line. It measures 180 degrees.

• system of equations

A system of equations is a set of two or more equations. Each equation contains two or more variables. We want to find values for the variables that make all the equations true.

These equations make up a system of equations:

$$\displaystyle \begin{cases} x + y = \text-2\\x - y = 12\end{cases}$$

The solution to this system is $$x=5$$ and $$y=\text-7$$ because when these values are substituted for $$x$$ and $$y$$, each equation is true: $$5+(\text-7)=\text-2$$ and $$5-(\text-7)=12$$.

• term

A term is a part of an expression. It can be a single number, a variable, or a number and a variable that are multiplied together. For example, the expression $$5x + 18$$ has two terms. The first term is $$5x$$ and the second term is 18.

• tessellation

A tessellation is a repeating pattern of one or more shapes. The sides of the shapes fit together perfectly and do not overlap. The pattern goes on forever in all directions.

This diagram shows part of a tessellation.

• transformation

A transformation is a translation, rotation, reflection, or dilation, or a combination of these.

• translation

A translation moves every point in a figure a given distance in a given direction.

This diagram shows a translation of Figure A to Figure B using the direction and distance given by the arrow.

• transversal

A transversal is a line that crosses parallel lines.

This diagram shows a transversal line $$k$$ intersecting parallel lines $$m$$ and $$\ell$$.

• two-way table

A two-way table provides a way to compare two categorical variables.

It shows one of the variables across the top and the other down one side. Each entry in the table is the frequency or relative frequency of the category shown by the column and row headings.

A study investigates the connection between meditation and the state of mind of athletes before a track meet. This two-way table shows the results of the study.

meditated did not meditate total
calm 45 8 53
agitated 23 21 44
total 68 29 97
• vertex

A vertex is a point where two or more edges meet. When we have more than one vertex, we call them vertices.

The vertices in this polygon are labeled $$A$$, $$B$$, $$C$$, $$D$$, and $$E$$.

• vertical angles

Vertical angles are opposite angles that share the same vertex. They are formed by a pair of intersecting lines. Their angle measures are equal.

For example, angles $$AEC$$ and $$DEB$$ are vertical angles. If angle $$AEC$$ measures $$120^\circ$$, then angle $$DEB$$ must also measure $$120^\circ$$.

Angles $$AED$$ and $$BEC$$ are another pair of vertical angles.

• vertical intercept

The vertical intercept is the point where the graph of a line crosses the vertical axis.

The vertical intercept of this line is $$(0,\text-6)$$ or just -6.

• volume

Volume is the number of cubic units that fill a three-dimensional region, without any gaps or overlaps.

For example, the volume of this rectangular prism is 60 units3, because it is composed of 3 layers that are each 20 units3.


text:
# A quantum mechanical description of a polarizing filter

When a single photon with polarization $\mathbf{a}$ arrives at a linear polarizing filter in the direction $\mathbf{p}$, the photon has a probability of $(\mathbf{a}\cdot\mathbf{p})^2$ to pass through the filter, while it has a probability of $1-(\mathbf{a}\cdot\mathbf{p})^2$ to be absorbed.

What does a typical quantum mechanical model of such a linear polarizing filter look like? In particular, I'm looking for how the quantized EM-field interacts with the many degrees of freedom in the filter. Also, any references to an article discussing such a model for a particular realistic polarizing filter would be appreciated.

• I don't know if this can be useful, but a beam splitter is in some sense a polarization filter (it deflects the radiation differently depending on the polarization), and it is extensively used in quantum optics. An example of its quantum modelization is for example this. Oct 1, 2014 at 15:37
• I guess you can model the system via a quantum operation. You will describe the filter as a collection of harmonic oscillators (the phonon field) and couple it to a mode of your quantum field (in canonical quantization the EM field is a collection of oscillators as well) through a coupling of the form a b^\dagger + a^\dagger b. a is the EM field annihilation operator of the relevant mode, and b is the collective annihilation operator of the phonons modes resonating with your field. Oct 1, 2014 at 15:47
• Intuitevely tracing over the filter degrees you will be left with a master equation describing the probability of absortion. I do not any reference about this though, maybe Nielsen and Chuang or quantum optics books. Oct 1, 2014 at 15:47
• The key thing to realize here is that the EM field is harmonic and usually in a coherent state. Because of this, interactions with the environment do not take the system out of the correspondance limit. For this reason, it turns out (not proving this in a comment) that you can just take the classical picture of loss and it's actually correct in the quantum description as well. You can see this because the interaction Hamiltonian between the photon and whatever else is $a$ on the photon, and the coherent state is an eigenstate of that operator. Oct 1, 2014 at 17:41
• On a broader level, you are essentially asking how to understand dissipation from a quantum mechanical picture. Excellent question! There is much literature about this if you Google "decoherence" or something like that, but maybe this simplified example will help you: physics.stackexchange.com/questions/36475/…. Oct 1, 2014 at 17:43


text:
# Time series forecast for small data set

I am new in data science so please accept my apology in advance if my question sounds stupid. I want to do a time series forecast of outage mins in the current regulatory year. The regulatory year starts from 1 April and ends on 30 March of next year. I have data of around six months i.e. from April to September. Outage does not occur every day. So I have only 144 data points (or days out of 171 days) where the outage occurred. I have plotted the data in the following graph. The graph shows the cumulative sum of outage mins.

Now I am trying to predict the value from October to March. I wanted to forecast the value that what would be the cumulative outage mins by the end of March next year. I tried to use Exponential smoothing but it did not work, it may be because I don't have a lot of observation. Then I was reading about ARIMA but not sure whether its the right algorithm to use or not as I don't think that there would be any seasonality in this scenario and also I don't have long data points. Could anyone help with which algorithm should I use to forecast the value? I am using Python as a programming language. Any help would be really appreciated.

ARIMA could work, I think it's the right approach. It's simple enough to be used on a small dataset, but sufficiently flexible at the same time. If you are using Python, library statsmodels allows you to implement ARIMA regressions. You have to grid search and find the right parameters to find the best fit, and run the prediction.
• There is a method, something like model.conf_int(), that will get you confidence intervals. – Leevo Sep 23 '20 at 7:26


text:
# Tag Info

5

This is conditioning in the sense of conditional probability. The idea is that the authors have some "standard physically-inspired features". They are splitting the data up into bins based on the values of these features, and then training a model for each bin. They are then examining the differences between the models. Usually this is done to learn ...

5

Perhaps the shortest answer to this question is that Bayes' Theorem itself allows us to easily change the direction of a conditional probability: $$P(A|B) = \frac{P(B|A)P(A)}{P(B)}$$ So if you have $P(B|A)$, $P(A)$, and $P(B)$, we can determine $P(A|B)$, and similarly you can determine $P(B|A)$ from $P(A|B)$, $P(B)$ and $P(A)$. Just by looking at $P(B|A)$...

3

But the conditional probability is clearly not symmetric and captures directed relationships. One needs to consider the kinds of directed relationships that is captured by conditional probability. It surely does capture some kind of association or dependence which could be directed. At the same time, it is not right to say that it surely captures the causal ...

2

This is the definition of conditional probability + Total probability decomposition formula: $p(y|x) = \frac{p(y,x}{p(x)} = \frac{p(x,y)}{\sum_{y'}p(x,y')}$. The idea is to use some unsupervised learning algorithm to learn the distribution $p(x,y)$ for every possible value of $y$, and by using the previous formula you can find $p(y|x)$.

Only top voted, non community-wiki answers of a minimum length are eligible


text:
# Expected value

#### Hans Rudel

##### New Member
Could someone please explain the following?

A guy and a girl play a game where they roll a dice. If the guy rolls an even number, the girl pays him that amount. If he rolls an odd number he pays her that amount.

The expected value is supposedly $0.5. ie mean of -1+2-3+4-5+6 but if i split the values like so girl: 1,3,5 total = 9 Average is 9/3 = 3 guy: 2,4,6 total = 12 Average = 12/3 = 4 dif = 1 and not 0.5 why can i not split up their winnings like the above? Thanks for your help #### Dason ##### Ambassador to the humans You can but you need to be more careful. Let X be the amount won on any given roll. $$E[X] = \sum XP(X)$$ $$= (-1)(1/6) + (2)(1/6) + (-3)(1/6) + (4)(1/6) + (-5)(1/6) + (6)(1/6)$$ $$= (1/6)(-1 +2 -3 +4 -5 +6)$$ $$= (1/6)(-1 -3 -5) + (1/6)(2 + 4 + 6)$$ [Here we separate the outcomes into either losing or winning] $$=(1/2)(-3) + (1/2)(4)$$ [Here I bring 1/3 into each of the sums to get the averages you have in your calculations] You need to account for the fact that you're losing$3 and that there is a probability of 1/2 of falling into either losing or winning. It's really that you didn't account for the probability of falling into losing or winning that messed you up here.

We can show something more general using a conditioning argument. Let $$I_W(X)$$ be an indicator of whether or not you win money on a given roll. We can use the fact that
E(X) = E[E(X|Y)] and what I showed up above is really just an application of this where $$Y=I_W(X)$$

#### Hans Rudel

##### New Member
Hey, thanks very much for replying to my post and clarifying my question.