text:
## The Homotopy Type Theory Book is out!

June 20, 2013

By now many of you have heard of the development of Homotopy Type Theory (HoTT), an extension of intuitionistic type theory that provides a natural foundation for doing synthetic homotopy theory.  Last year the Institute for Advanced Study at Princeton sponsored a program on the Univalent Foundations of Mathematics, which was concerned with developing these ideas.  One important outcome of the year-long program is a full-scale book presenting the main ideas of Homotopy Type Theory itself and showing how to apply them to various branches of mathematics, including homotopy theory, category theory, set theory, and constructive analysis.  The book is the product of a joint effort by dozens of participants in the program, and is intended to document the state of the art as it is known today, and to encourage its further development by the participation of others interested in the topic (i.e., you!).  Among the many directions in which one may take these ideas, the most important (to me) is to develop a constructive (computational) interpretation of HoTT.  Some partial results in this direction have already been obtained, including fascinating work by Thierry Coquand on developing a constructive version of Kan complexes in ITT, by Mike Shulman on proving homotopy canonicity for the natural numbers in a two-dimensional version of HoTT, and by Dan Licata and me on a weak definitional canonicity theorem for a similar two-dimensional theory.  Much work remains to be done to arrive at a fully satisfactory constructive interpretation, which is essential for application of these ideas to computer science.  Meanwhile, though, great progress has been made on using HoTT to formulate and formalize significant pieces of mathematics in a new, and strikingly beautiful, style, that are well-documented in the book.

The book is freely available on the web in various formats, including a PDF version with active references, an ebook version suitable for your reading device, and may be purchased in hard- or soft-cover from Lulu.  The book itself is open source, and is available at the Hott Book Git Hub.  The book is under the Creative Commons  CC BY-SA license, and will be freely available in perpetuity.

Readers may also be interested in the posts on Homotopy Type Theory, the n-Category Cafe, and Mathematics and Computation which describe more about the book and the process of its creation.

## Types and Cells

June 7, 2011

The doctrine of computational trinitarianism implies that there should be a categorial analogue of two-dimensional type theory … and indeed there is.  It is called, oddly enough, two-dimensional category theory, which arose first for numerous reasons.  What is two-dimensional category theory?  And how does it relate to two-dimensional type theory?

Two-dimensional category theory may be seen as an instance of the general concept of enriched categories in which the collection of morphisms between any two objects is endowed with some additional structure. A locally small category is one for which the maps between any two objects form a set, called the hom set.  An order-enriched category is one in which the morphisms form an ordered set, which is a set equipped with a pre-order (reflexive and transitive relation) on maps such that composition is monotone.  Order-enriched categories were used by Mitchell Wand and Gordon Plotkin and Mike Smyth in their development of the category-theoretic interpretation of recursive types.  Specifically, an O-category is an order-enriched category whose objects are cpo’s (pre-orders closed under sup’s of chains, and hence containing a least element) and whose hom sets are themselves cpo’s and for which composition is continuous (monotone and preserves suprema of chains).

More generally still, one may  consider (different forms of) category-enriched categories, in which the hom sets are structured as categories with their own vertical notion of identity and composition that meshes well with the horizontal notion of identity and composition of the category itself.  (I will not give here the precise meaning of “meshes well with”, since there are several possible notions and I will be discussing this structure in the type-theoretic setting below.)  The vertical maps are maps between maps that can be interpreted in several ways.  One way is as “witnesses” to an ordering relation among maps, viewing a category as a “pre-order with witnesses”, perhaps an approximation relation among maps such as arises in domain theory.  Another is to view these maps as homotopies between continuous functions on a space; these are the continuous deformations of one map into another.  (This is usually expressed by introducing a “time” coordinate ranging over the unit interval, and stating that a homotopy h between maps f and g is a continuous mapping such that at time zero h agrees with f, at time 1 agrees with g, and smoothly varies at times between.)  An important special case of category-enriched categories are those whose morphisms form (not just a category but also) a groupoid, a category in which each map is invertible.  These can be thought of as “equivalence relations with evidence”; the vertical maps are “proofs” that two horizontal maps are equivalent (for example, homotopic).

The sort of category-enriched categories that I have in mind are called (strict) 2-categories.  And as the terminology suggests, there is nothing special about the number 2 here; one can consider $n$-categories for any number $n$, and even $\infty$-categories that incorporate all of these into one grand structure (strictly or weakly).  To help manage this structure, the categorists have a uniform terminology that I wish to introduce here, called cells.  The objects in a category are the 0-cells, the maps are the 1-cells, the maps between maps (transformations, homotopies, …) are the 2-cells, and so forth.  A 2-category is one for which we stop at 2-cells; all higher cells being degenerate and hence ignored.  Often the 2-cells (and higher) form groupoids (in one of two senses that I will come back to later); a (2,1)-category is a 2-category in which the 2-cells form a groupoid (but the 1-cells need only form a category).  The class of $(\infty,1)$-categories are the subject of intense interest these days, in part because of their importance in homotopy theory.  They are, however, notoriously hard to manage, and, from what I understand, it is not yet clear what is even the correct definition.

Returning to two-dimensional type theory, and applying the types-as-categories correspondence, we get that types are 0-cells, terms (with free variables) are 1-cells, and transformations are 2-cells.  General terms are not invertible, but transformations are, giving rise to a (strict) groupoid structure expressed by the judgement $\alpha::M\simeq N:A$.  The rules for composition of transformations expresses the vertical structure as forming a strict groupoid.  Ordinary substitution expresses the horizontal structure of terms as maps (plugging in terms for free variables).  But how do these interact?  In strict two-dimensional type theory this interaction is expressed by definitional equalities that express the interchange law between horizontal and vertical composition.  Specifically, we have the following rule:

$\displaystyle{ {x:B\vdash \alpha::M\simeq N:A \qquad \vdash \beta::P\simeq Q:B}\over{\alpha[\beta]::\textit{map}\{x:B.A\}[\beta](M[P/x])\simeq N[Q/x]:A[Q/x]} }$

(More generally one must consider arbitrary contexts, and transformations between substitutions, but this instance of the general case expresses the essential idea.)

This “substitution” principle must satisfy some equational laws that amount to the following conditions:

1. Identity: $\alpha[\textit{id}]\equiv\alpha$.
2. Composition: $\alpha[\beta[\gamma]]\equiv \alpha[\beta][\gamma]$.
3. Interchange: $(\alpha\circ\alpha')[\beta\circ\beta'] = \alpha[\beta] \circ \textit{resp}\{map[\beta]\} (\alpha'[\beta'])$.
4. Delegation: $(\textit{id}_M)[\delta]\equiv M[\delta]$.

(Here $\textit{resp}$ is the application of a transformation to a term; it is there to “get the types right”.)  The interchange law is the type-theoretic analogue of the required interaction between 1-composition and 2-composition in a (strict) 2-category.

This is the judgmental structure of strict two-dimensional type theory.  There are several directions we can go from here.  One is to clarify the strict/weak distinction that has been underlying our discussions so far.  Another is to consider how to extend this to three- and higher-dimensional (or, dare I say it, infinite-dimensional) type theory.  The crucial ingredient for both of these discussions is one particular type constructor (more precisely, family of type constructors) that internalizes the hom structure as a type.  In the groupoidal case, where the higher structure is symmetric (invertible), this corresponds to (a version of) the Martin-Löf identity type.  The introduction rule is reflexivity, and the elimination rule is, in essence, the Yoneda Lemma from category theory.  When interpreted in terms of homotopy theory, this is the type of paths in a space, which is critical for defining the fundamental group(oid) of a space, and to clarifying the hinted-at distinction between weak and strict structure in higher dimensions.  More on that later!

## Transformations as strict groupoids

May 30, 2011

The distinguishing feature of higher-dimensional type theory is the concept of equivalence of the members of a type that must be respected by all families of types.  To be sufficiently general it is essential to regard equivalence as a structure, rather than a property.  This is expressed by the judgement

$\displaystyle \Gamma\vdash \alpha::M\simeq N:A$

which states that $M$ and $N$ are equivalent members of type $A$, as evidenced by the transformation $\alpha$.  Respect for equivalence is ensured by the rule

$\displaystyle{{\Gamma,x:A\vdash B\,\textsf{type}\quad \Gamma\vdash \alpha :: M\simeq N:A \quad \Gamma\vdash P:B[M/x]}\over {\Gamma\vdash \textit{map}\{x:A.B\}[\alpha](P):B[N/x]}},$

which states that equivalent members determine equivalent instances of a family of types.  The equivalence between instances is mediated by the operation $\textit{map}\{x:A.B\}[\alpha](-)$, which sends members of $B[M/x]$ to members of $B[N/x]$.  We call this mapping the action of the family $x:A.B$ on the transformation $\alpha$.

For reasons that will only become apparent as we go along, it is important that “equivalence” really be an equivalence: it must be, in an appropriate sense, reflexive, symmetric, and transitive.  The “appropriate sense” is precisely that we require the existence of transformations

$\displaystyle{\Gamma\vdash \textit{id}::M\simeq M:A}$

$\displaystyle{{\Gamma\vdash\alpha::M\simeq N:A}\over{\Gamma\vdash\alpha^{-1}::N\simeq M:A}}$

$\displaystyle{{\Gamma\vdash \beta:N\simeq P:A\quad \Gamma\vdash \alpha:M\simeq N:A}\over{\Gamma\vdash\beta\circ\alpha:M\simeq P:A}}$

Moreover, these transformations must be respected by the action of any family, in a sense that we shall make clear momentarily.  Before doing so, let us observe that these transformations constitute the operations of a groupoid, which we may think of either as an equivalence relation equipped with evidence or a category in which every map is invertible (a generalized group).  While the former interpretation may not suggest it, the latter formulation implies that we should impose some requirements on how these transformations interact, namely the axioms of a groupoid:

1. Composition (multiplication) is associative: $\gamma\circ(\beta\circ\alpha)\equiv (\gamma\circ\beta)\circ\alpha::M\simeq N:A$.
2. Identity is the unit of composition: $\textit{id}\circ\alpha\equiv\alpha::M\simeq N:A$ and $\alpha\circ\textit{id}\equiv\alpha::M\simeq N:A$.
3. Inverses cancel: $\alpha^{-1}\circ\alpha\equiv\textit{id}::M\simeq M:A$ and $\alpha\circ\alpha^{-1}\equiv\textit{id}::N\simeq N:A$.
These conditions, which impose equalities on transformations, demand that the second-dimensional structure of a type form a strict groupoid.  I will come back to an important weakening of these requirements later.

We further require that the action of a type family preserve the groupoid structure.  For this it is enough to require that it preserve identities and composition:

$\displaystyle{\textit{map}\{x:A.B\}[\textit{id}](-) \equiv \textit{id}(-):B[M/x]}$

and

$\displaystyle{\begin{array}{c}\textit{map}\{x:A.B\}[\beta\circ\alpha](-)\\\equiv\\\textit{map}\{x:A.B\}[\beta](\textit{map}\{x:A.B\}[\alpha](-))\end{array}}$.

Thinking of a groupoid as a category, these conditions state that the action of a type family be (strictly) functorial.  (Here again we are imposing strong requirements in order to facilitate the exposition; eventually we will consider a relaxation of these conditions that will admit a richer range of applications.)

(The alert reader will note that I have not formally introduced the concept of a transformation between types, nor the equality of these, into the theory.  There are different ways to skin this cat; for now, I will be a bit loose about the axiomatics in order to focus attention on the main ideas.  Rest assured that everything can be made precise!)

By demanding that the groupoid axioms hold strictly (as equalities) and that the action of families be strictly functorial, we have simplified the theory considerably by restricting it to dimension 2.  To relax these restrictions requires higher dimensions.  For example, we may demand only that the groupoid conditions hold up to a transformation of transformations, but hold strictly from then on; this is the 3-dimensional case.  Or we can relax all such conditions to hold only up to a higher transformation, resulting in finite dimensional type theory.  Similar considerations will apply to other conditions that we shall impose on the action of families, in particular to specify the action of type constructors on transformations, which I will discuss next time.  The presentation of finite-dimensional type theory will be aided by the introduction of identity types (also called path types).  Identity types avoid the need for an ever-expanding nesting of transformations between transformations between ….  More on that later!

Update (August 2012): Egbert Rijke has written lucidly on the topic of Yoneda’s Lemma and it’s relation to homotopy type theory in his Master’s Thesis, which I encourage readers to consult for a nice summary of higher-dimensional type theory.

## Higher-Dimensional Type Theory

May 30, 2011

Ideas have their time, and it’s not for us to choose when they arrive.  But when they do, they almost always occur to many people at more or less the same time, often in a slightly disguised form whose underlying unity becomes apparent only later.  This is perhaps not too surprising, the same seeds taking root in many a fertile mind.  A bit harder to explain, though, is the moment in time when an idea comes to fruition.  Often all of the ingredients are available, and yet no one thinks to put two-and-two together and draw what seems, in retrospect, to be the obvious inference.  Until, suddenly, everyone does.  Why didn’t we think of that ages ago?  Nothing was stopping us, we just didn’t notice the opportunity!

The recent development of higher-dimensional structure in type theory seems to be a good example.  All of the ingredients have been present since the 1970′s, yet as far as I know no one, until quite recently, no one quite put together all the pieces to expose the beautiful structure that has been sitting there all along.  Like many good ideas, one can see clearly that the ideas were foreshadowed by many earlier developments whose implications are only now becoming understood.  My plan is to explain higher type theory (HTT) to the well-informed non-expert, building on ideas developed by various researchers, including Thorsten Altenkirch, Steve Awodey, Richard Garner, Martin Hofmann, Dan Licata, Peter Lumsdaine, Per Martin-Löf, Mike Shulman, Thomas Streicher, Vladimir Voevodsky, and Michael Warren.  It will be useful in the sequel to be familiar with The Holy Trinity, at least superficially, and preferably well enough to be able to move back and forth between the three manifestations that I’ve previously outlined.

One-dimensional dependent type theory is defined by derivation rules for these four fundamental forms of judgement (and, usually, some others that we suppress here for the sake of concision):

$\displaystyle \Gamma\vdash A\,\mathsf{type}$

$\displaystyle \Gamma\vdash M : A$

$\displaystyle \Gamma\vdash M \equiv N : A$

$\displaystyle \Gamma\vdash A\equiv B$

A context, $\Gamma$, consists of a sequence of declarations of variables of the form $x_1:A_1,\dots,x_n:A_n$, where it is presupposed, for each $1\leq i\leq n$, that $x_1:A_1,\dots,x_{i-1}:A_{i-1}\vdash A_i\,\mathsf{type}$ is derivable.

The key notion of dependent type theory is that of a family of types indexed by (zero or more) variables ranging over a type.  The judgement $\Gamma\vdash A\,\mathsf{type}$ states that $A$ is a family of types indexed by the variables given by $\Gamma$.  For example, we may have $\vdash\textit{Nat}\,\textsf{type}$, specifying that $\textit{Nat}$ is a closed type (a degenerate family of types), and $x{:}\textit{Nat}\vdash\textit{Seq}(x)\,\textsf{type}$, specifying that $\textit{Seq}(n)$ is a type (say, of sequences of naturals of length $n$) for each $\vdash n:\textit{Nat}$.  The rules of type theory ensure, either directly or indirectly, that the structural properties of the hypothetical/general judgement are valid.  In particular families of types respect equality of indices:

$\displaystyle{{\Gamma,x:A\vdash B\,\textsf{type}\quad \Gamma\vdash M\equiv N:A \quad \Gamma\vdash P:B[M/x]}\over {\Gamma\vdash P:B[N/x]}}.$

In words, if $B$ is a family of types indexed by $A$, and if $M$ and $N$ are equal members of type $A$, then every member of $B[M/x]$ is also a member of $B[N/x]$.

The generalization to two- (and higher-) dimensional type theory can be motivated in several ways.  One natural source of higher-dimensional structure is a universe, a type whose elements correspond to types.  For example, we may have a universe of sets given as follows:

$\displaystyle \vdash \textit{Set}\,\textsf{type}$

$\displaystyle x:\textit{Set}\vdash \textit{Elt}(x)\,\textsf{type}$

$\displaystyle \vdash \textit{nat}:\textit{Set}$

$\displaystyle \vdash \textit{Elt}(\textit{nat})\equiv\textit{Nat}$

$\displaystyle a:\textit{Set},b:\textit{Set}\vdash a\times b : \textit{Set}$

$\displaystyle a:\textit{Set},b:\textit{Set}\vdash \textit{Elt}(a\times b)\equiv \textit{Elt}(a)\times\textit{Elt}(b)$

and so forth, ensuring that $\textit{Set}$ is closed under typical set-forming operations whose interpretations are given by $\textit{Elt}$ in terms of standard type-theoretic concepts.

In many situations, including much of informal (yet entirely rigorous) mathematics, it is convenient to identify sets that are isomorphic, so that, for example, the sets $\textit{nat}\times\textit{nat}$ and $\textit{2}\to\textit{nat}$ would be interchangeable.  In particular, these sets should have the “same” (type of) elements.  But obviously these two sets do not have the same elements (one consists of pairs, the other of functions, under the natural interpretation of the sets as types), so we cannot hope to treat $\textit{Elt}(\textit{nat}\times\textit{nat})$ and $\textit{Elt}(\textit{2}\to\textit{nat})$ as equal, though we may wish to regard them as equivalent in some sense.  Moreover, since two sets can be isomorphic in different ways, isomorphism must be considered a structure on sets, rather than a property of sets.  For example, $\textit{2}$ is isomorphic to itself in two different ways, by the identity and by negation (swapping).  Thus, equivalence of the elements of two isomorphic sets must take account of the isomorphism itself, and hence must have computational significance.

It is precisely the desire to accommodate equivalences such as this that gives rise to higher dimensions in type theory.  Specifically, we introduce two-dimensional structure by adding a new judgement to type theory stating that two members of a type are related by a specified transformation:

$\displaystyle \Gamma\vdash \alpha :: M\simeq N : A$

Crucially, families of types must respect transformation:

$\displaystyle{{\Gamma,x:A\vdash B\,\textsf{type}\quad \Gamma\vdash \alpha :: M\simeq N:A \quad \Gamma\vdash P:B[M/x]}\over {\Gamma\vdash \textit{map}\{x:A.B\}[\alpha](P):B[N/x]}}.$

A transformation should be thought of as evidence of interchangeability of the members of a type; the map operation puts the evidence to work.

Returning to our example of the universe of sets, let us specify that a transformation from one set to another is an pair of functions constituting a bijection between the elements of the two sets:

$\displaystyle{ {\begin{array}{c} \Gamma,x:\textit{Elt}(a)\vdash f(x):\textit{Elt}(b) \\ \Gamma,x:\textit{Elt}(b)\vdash g(x):\textit{Elt}(a) \\ \Gamma,x:\textit{Elt}(a)\vdash g(f(x))\equiv x:\textit{Elt}(a) \\ \Gamma,x:\textit{Elt}(b)\vdash f(g(x))\equiv x:\textit{Elt}(b) \end{array}} \over {\Gamma\vdash\textit{iso}(f,g)::a\simeq b:\textit{Set}}}$

(The equational conditions here are rather strong; I will return to this point in a future post.  For now, let us just take this as the defining criterion of isomorphism between two sets.)

Evidence for the isomorphism of two sets induces a transformation on types given by the following equation:

$\displaystyle{ {\Gamma\vdash M:\textit{Elt}(a)}\over {\Gamma\vdash \textit{map}\{\textit{Elt}\}[\textit{iso}(f,g)](M)\equiv f(M) : \textit{Elt}(b)}}$

(suppressing the obvious typing premises for $f$ and $g$).  In words an isomorphism between sets $a$ and $b$ induces a transformation between their elements given by the isomorphism itself.

This, then, is the basic structure of two-dimensional type theory, but there is much more to say!  In future posts I intend to develop the ideas further, including a discussion of these topics:

1. The definition of $\textit{map}\{x:A.B\}$ is given by induction over the structure of $x:A.B$.  The above equation covers only one case; there are more, corresponding to each way of forming a family of types $x:A.B$.  The extension to function types will expose the role of the inverse of the isomorphism between sets.
2. The judgement $\alpha::M\simeq N:A$ may be internalized as a type, which will turn out to correspond to the identity type in Martin-Löf’s type theory, albeit with a different interpretation given by Altenkirch.  The identity type plays an important role in the extension to all higher dimensions.
3. To ensure coherence and to allow for greater expressiveness we must also discuss equality and equivalence of transformations and how these influence the induced transformation of families of types.  In particular transformations admit a groupoid structure which expresses reflexivity, symmetry, and transitivity of transformation; these conditions can be considered to hold strongly or weakly, giving rise to different applications and interpretations.
4. Higher-dimensional type theory admits a fascinating interpretation in terms of homotopy theory which types are interpreted as spaces, members as points in those spaces, and transformations as paths, or homotopies.  This, together with a generalization of the treatment of universes outlined above, is the basis for Voevodsky’s work on univalent foundations of mathematics.
5. One may consider relaxing the groupoid structure on transformations to a “monoidoid” (that is, category) structure by not requiring symmetry (inverses).  The structure of type theory changes significantly in the absence of symmetry, posing significant open problems, but admitting a wider range of applications of higher-dimensional structure in both CS and mathematics.
To keep up to date with the latest developments in this area, please visit the Homotopy Type Theory blog!

## The Holy Trinity

March 27, 2011

The Christian doctrine of trinitarianism states that there is one God that is manifest in three persons, the Father, the Son, and the Holy Spirit, who together form the Holy Trinity.   The doctrine of computational trinitarianism holds that computation manifests itself in three forms: proofs of propositions, programs of a type, and mappings between structures.  These three aspects give rise to three sects of worship: Logic, which gives primacy to proofs and propositions; Languages, which gives primacy to programs and types; Categories, which gives primacy to mappings and structures.  The central dogma of computational trinitarianism holds that Logic, Languages, and Categories are but three manifestations of one divine notion of computation.  There is no preferred route to enlightenment: each aspect provides insights that comprise the experience of computation in our lives.

Computational trinitarianism entails that any concept arising in one aspect should have meaning from the perspective of the other two.  If you arrive at an insight that has importance for logic, languages, and categories, then you may feel sure that you have elucidated an essential concept of computation—you have made an enduring scientific discovery.  Advances in our understanding of computation may arise from insights gained in many ways (any data is useful and relevant), but their essential truth does not depend on their popularity.

Logic tells us what propositions exist (what sorts of thoughts we wish to express) and what constitutes a proof (how we can communicate our thoughts to others).  Languages (in the sense of programming) tells us what types exist (what computational phenomena we wish to express) and what constitutes a program (how we can give rise to that phenomenon).  Categories tell us what structures exist (what mathematical models we have to work with) and what constitutes a mapping between them (how they relate to one another).  In this sense all three have ontological force; they codify what is, not how to describe what is already given to us.  In this sense they are foundational; if we suppose that they are merely descriptive, we would be left with the question of where these previously given concepts arise, leading us back again to foundations.  It is the foundations that I wish to describe here, because I believe it will help to clarify some common misunderstandings about the notions of proposition, type, and structure.  Of particular interest here is that a “type system” is not, under this conception, an arbitrary collection of conditions imposed on a previously given notion of program (whether written with horizontal lines, or not).  It is, rather, a way to say what the programs are in the first place, and what they mean as proofs and as mappings.

Here I will outline the basic correspondences between logic, languages, and categories by examining their structural properties (and, for now, nothing more).

The fundamental notion in logic is that of entailment, written $P_1,\dots,P_n\vdash P$, expressing derivability of $P$ from $P_1,\dots, P_n$.  This means that $P$ is derivable from the rules of logic, given the $P_i$ as axioms.  In contrast to admissibility (which I will not discuss further here) this form of entailment does not express implication!  In particular, an entailment is never vacuously true.  Entailment enjoys at least two crucial structural properties, making it a pre-order:

$\displaystyle{\strut\over{P\vdash P}}$

$\displaystyle{{P\vdash Q\quad Q\vdash R}\over{P\vdash R}}$.

$\displaystyle{{P_1,\dots,P_n\vdash Q}\over{P_1,\dots,P_n,P_{n+1}\vdash Q}}$

$\displaystyle{{P_1,\dots,P_i,P_{i+1},\dots,P_n\vdash Q}\over{P_1,\dots,P_{i+1},P_{i},\dots,P_n\vdash Q}}$

$\displaystyle{{P_1,\dots,P_i,P_i,\dots,P_n\vdash Q}\over{P_1,\dots,P_i,\dots,P_n\vdash Q}}$.

These state that “extra” axioms do not affect deduction; the “order” of axioms does not matter; “duplication” of axioms does not matter.  (These may seem inevitable, but in substructural logics any or all of these may be denied.)

In languages we have the fundamental concept of a typing judgement, written $x_1{:}A_1,\dots,x_n{:} A_n\vdash M{:}A$, stating that $M$ is an expression of type $A$ involving variables $x_i$ of type $A_i$.  A typing judgement must satisfy the following basic structural properties:

$\displaystyle{\strut\over{x:A\vdash x:A}}$

$\displaystyle{{y:B\vdash N:C \quad x:A\vdash M:B}\over{x:A\vdash [M/y]N:C}}$

We may think of the variables as names for “libraries”, in which case the first states that we may use any library we wish, and the second states closure under “linking” (as in the Unix tool ld or its relatives), with $[M/x]N$ being the result of linking $x$ in $N$ to the library $M$.  Typically we expect analogues of the “extra”, “reordering”, and “duplication” axioms to hold as well, though this ain’t necessarily so.  I will leave their formulation as an exercise for the reader.

In categories we have the fundamental concept of a mapping $f:X\longrightarrow Y$ between structures $X$ and $Y$.  The most elementary structures, perhaps, are sets, and mappings are functions, but it is more common to consider, say, that $X$ and $Y$ are topological spaces, and $f$ is a continuous function between them.  Mappings satisfy analogous structural properties:

$\displaystyle{\strut\over{\textit{id}_X : X \longrightarrow X}}$

$\displaystyle{{f:X\longrightarrow Y \quad g : Y\longrightarrow Z}\over{g\circ f:X\longrightarrow Z}}$

These express, respectively, the existence of the identity map, and the closure of maps under composition.  They correspond to reflexivity and transitivity of entailment, and to the library and linking rule of languages.  As with types, one may expect additional closure conditions corresponding to the “extra”, “reordering”, and “duplication” axioms by giving suitable meaning to multiple assumptions.  I will not go into this here, but numerous standard sources treat these conditions in detail.

What I find captivating about computational trinitarianism is that it is beautiful!  Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!  Imagine a world in which the code is the math, in which there is no separation between the reasoning and the execution, no difference between the language of mathematics and the language of computing.  Trinitarianism is the central organizing principle of a theory of computation that integrates, unifies, and enriches the language of logic, programming, and mathematics.  It provides a framework for discovery, as well as analysis, of computational phenomena.  An innovation in one aspect must have implications for the other; a good idea is a good idea, in whatever form it may arise.  If an idea does not make good sense logically, categorially, and typically (sorry for the neologism), then it cannot be a manifestation of the divine.

Follow


text:
# How to memoize with patterns? [duplicate]

Here is an artificial example to explain what I am up to. Define

ClearAll[f]
f[x_, y_] := f[x, y] = If[x == 0, g[y], g[f[x - 1, y]]]

Then AbsoluteTiming[f[10, y]] gives

{0.0000863, g[g[g[g[g[g[g[g[g[g[g[y]]]]]]]]]]]},

whereafter AbsoluteTiming[f[5, y]] gives

{6.2*10^-6, g[g[g[g[g[g[y]]]]]]}.

However after that AbsoluteTiming[f[5, z]] gives

{0.0000487, g[g[g[g[g[g[z]]]]]]},

i. e. with z it takes more time than with y. This is because the remembered downvalues of f before evaluating at z only involve the variable y - for example, HoldPattern[f[2, y]] :> g[g[g[y]]] is among them.

If I could memoize something like HoldPattern[f[2, y_]] :> g[g[g[y]]] instead (that is, with pattern y_ instead of the hardwired variable y), would not the result be more efficient? If no, why? If yes, how to do it?

format: plain


text:
Faculté des sciences

## Structure and electronic structure of quasicrystal and approximant surfaces: a photoemission study

### In: Progress in Surface Science, 2004, vol. 75, p. 205-225

The structure and electronic structure of different high-symmetry surfaces of either quasicrystalline or approximant Al–Pd–Mn were studied by means of photoemission-based techniques such as X-ray photoelectron diffraction (XPD) and ultraviolet photoelectron spectroscopy. We find that the twofold (2f), 3f and 5f surfaces of icosahedral Al–Pd–Mn exhibit all the symmetry elements of the... More


text:
# Calculate gravitational acceleration in a vacuum?

1. Feb 21, 2013

### rockchalk1312

The gravitational acceleration in vacuum varies with latitude, elevation, and local inhomogeneities in the earth's crust. Use the following equation to find g in Lawrence based on a latitude of λ=38°57' ±3' and an elevation of H=259±10m. Calculate the uncertainty using the total difference.

g = 9.780556m/s2[1+0.0052885sin2λ-0.0000059sin2(2λ)]-0.0000020s-2H

How do you include latitude when it's at three different dimensions? And I know the total difference formula but how would you put it in here exactly? Thank you very much for any help!

2. Feb 21, 2013

### cepheid

Staff Emeritus
The latitude is being expressed in degrees (°), arcminutes ('), and arcseconds ("), where:

1 arcmin = (1/60) degrees

1 arcsec = (1/60) arcmins

3. Feb 21, 2013

### haruspex

I assume that's a formula you've been given, so it's obvious how to use the latitude and altitude in computing g. That leaves me not knowing what you're asking. Are you puzzled as to how the formula can be valid?
When asked to compute an uncertainty in f=f(x,y,..), given the uncertainties in x, y..., there are two principal methods producing different answers: absolute uncertainty and statistical uncertainty. The first is appropriate when the given uncertainties are absolute uncertainties with uniform distributions (as often is the case with instrumental measurements), there are only two or three parameters, and the answer is to be relied on absolutely, as may be the case in structural engineering. In this method, just plug in all the combinations of extreme values for the parameters and see what f values come out.
For statitical uncertainty you assume the given uncertainties are some number of standard deviations, the same number in each parameter, or otherwise convert to that form. You may then be able to use a root-sum-square formula to combine them, and the answer will represent the same number of standard deviations for f.
E.g. if f=x*y, Δf = xΔy+yΔx; E[(Δf)2] = E[x2]Δy2+E[y2]Δx2; σ(f)/f = √((σ(x)/x)2+(σ(y)/y)2).
More generally, Δf = (∂f/∂x)Δx+(∂f/∂y)Δy, etc.


text:
# Glossary for Lesson 33: Solving Exponential and Logarithmic Equations

### Product property

The product property of logarithms can be stated as the following:
\log_aAB=\log_aA+\log_bB

### Quotient property

The quotient property of logarithms can be stated as the following:
\log_a\frac{A}{B}=\log_aA-\log_aB

### Power Property

The power property of logarithms can be stated as the following:
\log_aA^n=n\log_aA

### Change of Base Formula

In order to change the base of a logarithmic expression without changing its value, we can use the change of base formula:
\log_ax=\frac{\log_bx}{\log_ba}

### One-to-One Properties of Exponents and Logs

a^x=a^y if and only if x=y
\log_ax=\log_ay if and only if x=y

a^{\log_ax}=x
\log_aa^x=x


text:
# characteristic polynomial

## EnglishEdit

### NounEdit

1. (linear algebra) The determinant, of a matrix minus an indeterminant times the identity matrix
The characteristic polynomial of ${\displaystyle \left({\begin{array}{cc}1&4\\3&-5\end{array}}\right)}$  is ${\displaystyle \mathbf {Det} \left({\begin{array}{cc}1-x&4\\3&-5-x\end{array}}\right)}$ .

#### Usage notesEdit

Equally many authors instead subtract the matrix from the indeterminant times the identity matrix. But the result only differs by multiplication by -1, which isn't important where characteristic polynomials are studied.


text:
+0

# This is too confsing

-1
106
5
+172

What is the smallest positive integer n such that $$3n \equiv 1356 \pmod{22}?$$

Jul 13, 2020

#1
+744
+1

only try to post a few or a single questions at a time, please

Jul 13, 2020
#3
+279
0

yeah forumofweb2.0cal do your own homework

#4
+2313
+1

I think this is Alcumus....

CalTheGreat  Jul 13, 2020
#2
0

I think it is 12.

Jul 13, 2020
#5
+25543
+1

What is the smallest positive integer n such that  $$3n \equiv 1356 \pmod{22}$$

$$\begin{array}{|rcll|} \hline 3n &\equiv& 1356 \pmod{22} \\ 3n &\equiv& 1356-61*22 \pmod{22} \\ 3n &\equiv& 14 \pmod{22} \\ n &\equiv& \dfrac{14}{3} \pmod{22} \\ n &\equiv& 14*3^{-1} \pmod{22} \\ && \boxed{ 3^{-1} \pmod{22} = 3^{\phi(22)-1} \pmod{22} \quad | \quad \phi(22)=22*\left( 1-\dfrac{1}{2}\right)*\left( 1-\dfrac{1}{11}\right)=10 \\ =3^{10-1} \pmod{22} \\ = 3^9 \pmod{22} \\ = 19683 \pmod{22} \\ = 19683-894*22 \pmod{22} \\ = 15 \pmod{22} \\\mathbf{3^{-1} \pmod{22}=15 \pmod{22}} } \\ n &\equiv& 14*15 \pmod{22} \\ n &\equiv& 210 \pmod{22} \\ n &\equiv& 210-9*22 \pmod{22} \\ \mathbf{n} &\equiv& \mathbf{12 \pmod{22}} \\ \hline \end{array}$$

The smallest positive integer n is $$\mathbf{12}$$

Jul 14, 2020
edited by heureka  Jul 14, 2020


text:
# Sørensen–Dice coefficient

(Redirected from Dice's coefficient)
Jump to: navigation, search

The Sørensen–Dice index, also known by other names (see Name, below), is a statistic used for comparing the similarity of two samples. It was independently developed by the botanists Thorvald Sørensen[1] and Lee Raymond Dice,[2] who published in 1948 and 1945 respectively.

## Name

The index is known by several other names, especially the Sørensen index and Dice's coefficient. Other variations include the "similarity coefficient" or "index", such as Dice similarity coefficient (DSC). Common alternate spellings for Sørensen are Sorenson, Soerenson and Sörenson, and all three can also be seen with the –sen ending.

Other names include:

## Formula

Sørensen's original formula was intended to be applied to presence/absence data, and is

${\displaystyle QS={\frac {2|X\cap Y|}{|X|+|Y|}}}$

where |X| and |Y| are the numbers of elements in the two samples. Based on what is written here,

${\displaystyle DSC={\frac {2TP}{2TP+FP+FN}}}$,

as compared with the Jaccard index, which only counts true positives once in both the numerator and denominator. QS is the quotient of similarity and ranges between 0 and 1.[7] It can be viewed as a similarity measure over sets.

Similarly to the Jaccard index, the set operations can be expressed in terms of vector operations over binary vectors A and B:

${\displaystyle s_{v}={\frac {2|A\cdot B|}{|A|^{2}+|B|^{2}}}}$

which gives the same outcome over binary vectors and also gives a more general similarity metric over vectors in general terms.

For sets X and Y of keywords used in information retrieval, the coefficient may be defined as twice the shared information (intersection) over the sum of cardinalities :[8]

When taken as a string similarity measure, the coefficient may be calculated for two strings, x and y using bigrams as follows:[9]

${\displaystyle s={\frac {2n_{t}}{n_{x}+n_{y}}}}$

where nt is the number of character bigrams found in both strings, nx is the number of bigrams in string x and ny is the number of bigrams in string y. For example, to calculate the similarity between:

night
nacht

We would find the set of bigrams in each word:

{ni,ig,gh,ht}
{na,ac,ch,ht}

Each set has four elements, and the intersection of these two sets has only one element: ht.

Inserting these numbers into the formula, we calculate, s = (2 · 1) / (4 + 4) = 0.25.

## Difference from Jaccard

This coefficient is not very different in form from the Jaccard index. In fact, both are equivalent in the sense that given a value for the Sørensen–Dice coefficient ${\displaystyle S}$, one can calculate the respective Jaccard index value ${\displaystyle J}$ and vice versa, using the equations ${\displaystyle J=S/(2-S)}$ and ${\displaystyle S=2J/(1+J)}$.

Since the Sørensen–Dice coefficient doesn't satisfy the triangle inequality, it can be considered a semimetric version of the Jaccard index.[3]

The function ranges between zero and one, like Jaccard. Unlike Jaccard, the corresponding difference function

${\displaystyle d=1-{\frac {2|X\cap Y|}{|X|+|Y|}}}$

is not a proper distance metric as it does not possess the property of triangle inequality.[3] The simplest counterexample of this is given by the three sets {a}, {b}, and {a,b}, the distance between the first two being 1, and the difference between the third and each of the others being one-third. To satisfy the triangle inequality, the sum of any two of these three sides must be greater than or equal to the remaining side. However, the distance between {a} and {a,b} plus the distance between {b} and {a,b} equals 2/3 and is therefore less than the distance between {a} and {b} which is 1.

## Applications

The Sørensen–Dice coefficient is useful for ecological community data (e.g. Looman & Campbell, 1960[10]). Justification for its use is primarily empirical rather than theoretical (although it can be justified theoretically as the intersection of two fuzzy sets[11]). As compared to Euclidean distance, the Sørensen distance retains sensitivity in more heterogeneous data sets and gives less weight to outliers.[12] Recently the Dice score (and its variations, e.g. logDice taking a logarithm of it) has become popular in computer lexicography for measuring the lexical association score of two given words.[13] It is also commonly used in image segmentation, in particular for comparing algorithm output against reference masks in medical applications.[6]

## Abundance version

The expression is easily extended to abundance instead of presence/absence of species. This quantitative version is known by several names:

## References

1. ^ Sørensen, T. (1948). "A method of establishing groups of equal amplitude in plant sociology based on similarity of species and its application to analyses of the vegetation on Danish commons". Kongelige Danske Videnskabernes Selskab. 5 (4): 1–34.
2. ^ Dice, Lee R. (1945). "Measures of the Amount of Ecologic Association Between Species". Ecology. 26 (3): 297–302. doi:10.2307/1932409. JSTOR 1932409.
3. Gallagher, E.D., 1999. COMPAH Documentation, University of Massachusetts, Boston
4. ^ Prescott, J.W.; Pennell, M.; Best, T.M.; Swanson, M.S.; Haq, F.; Jackson, R.; Gurcan, M.N. (2009). An automated method to segment the femur for osteoarthritis research. IEEE. doi:10.1109/iembs.2009.5333257.
5. ^ Swanson, M.S.; Prescott, J.W.; Best, T.M.; Powell, K.; Jackson, R.D.; Haq, F.; Gurcan, M.N. (2010). "Semi-automated segmentation to assess the lateral meniscus in normal and osteoarthritic knees". Osteoarthritis and Cartilage. Elsevier BV. 18 (3): 344–353. doi:10.1016/j.joca.2009.10.004. ISSN 1063-4584.
6. ^ a b Zijdenbos, A.P.; Dawant, B.M.; Margolin, R.A.; Palmer, A.C. (1994). "Morphometric analysis of white matter lesions in MR images: method and validation". IEEE Transactions on Medical Imaging. Institute of Electrical and Electronics Engineers (IEEE). 13 (4): 716–724. doi:10.1109/42.363096. ISSN 0278-0062. PMID 18218550.
7. ^ http://www.sekj.org/PDF/anbf40/anbf40-415.pdf
8. ^ van Rijsbergen, Cornelis Joost (1979). Information Retrieval. London: Butterworths. ISBN 3-642-12274-4.
9. ^ Kondrak, Grzegorz; Marcu, Daniel; Knight, Kevin (2003). "Cognates Can Improve Statistical Translation Models" (PDF). Proceedings of HLT-NAACL 2003: Human Language Technology Conference of the North American Chapter of the Association for Computational Linguistics. pp. 46–48.
10. ^ Looman, J.; Campbell, J.B. (1960). "Adaptation of Sorensen's K (1948) for estimating unit affinities in prairie vegetation". Ecology. 41 (3): 409–416. JSTOR 1933315.
11. ^ Roberts, D.W. (1986). "Ordination on the basis of fuzzy set theory". Vegetatio. 66 (3): 123–131. doi:10.1007/BF00039905.
12. ^ McCune, Bruce & Grace, James (2002) Analysis of Ecological Communities. Mjm Software Design; ISBN 0-9721290-0-6.
13. ^ Rychlý, P. (2008) A lexicographer-friendly association score. Proceedings of the Second Workshop on Recent Advances in Slavonic Natural Language Processing RASLAN 2008: 6–9
14. ^ Bray, J. Roger; Curtis, J. T. (1957). "An Ordination of the Upland Forest Communities of Southern Wisconsin". Ecological Monographs. 27 (4): 326–349. doi:10.2307/1942268.


text:
# Solving Sudoku (again)

More Rust! This time, I want to go back to my post on A Generic Brute Force Backtracking Solver. For one, because I’m learning Rust. For two, because there is a crate specifically for im mutable data structures. And for three, because I expect it will be much faster. We shall see!

## Representing the board

As one does, we’re going to start with Sudoku. So to do that, we’ll need to represent the board. Because it’s just a 9x9 grid, I’m going to use Rust arrays:

#[derive(Copy, Clone, Debug)]
struct Sudoku {
board: [[u8; 9]; 9]
}

And because I want a decent display function:

impl fmt::Display for Sudoku {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
let mut s: String = String::new();

s += "sudoku:\n";
for x in 0..9 {
s += "  ";
for y in 0..9 {
if self.board[x][y] == 0 {
s += " ";
} else {
// This seems weird
s = format!("{}{}", s, self.board[x][y]);
}

if y == 2 || y == 5 {
s += "|";
}
}
s += "\n";

if x == 2 || x == 5 {
s += "  ---+---+---\n";
}
}

write!(f, "{}", s)
}
}

If there’s a better way to do that… I’d love to here it. In particular, I couldn’t figure out a better way to put in the u8 to String bit without borrowing issues. Rust yo.

So now I can create an initial board:

let initial_state = Sudoku {
board: [
[0, 0, 0, 2, 6, 0, 7, 0, 1],
[6, 8, 0, 0, 7, 0, 0, 9, 0],
[1, 9, 0, 0, 0, 4, 5, 0, 0],
[8, 2, 0, 1, 0, 0, 0, 4, 0],
[0, 0, 4, 6, 0, 2, 9, 0, 0],
[0, 5, 0, 0, 0, 3, 0, 2, 8],
[0, 0, 9, 3, 0, 0, 0, 7, 4],
[0, 4, 0, 0, 5, 0, 0, 3, 6],
[7, 0, 3, 0, 1, 8, 0, 0, 0]
]
};

I’ll use 0 for the empty spaces and the numbers for everything else. Cool. So next?

## A State trait

Next, we need something to solve. The idea of defining a generic function in Rust that can operate over different sorts of problems fits perfectly into traits, so let’s make one:

pub trait State {
fn next_states(self) -> Option<Vec<Self>> where Self: Sized + Copy;

fn is_valid(self) -> bool;
fn is_solved(self) -> bool;
}

For something to be a State, it needs to have three functions defined:

• next_states - takes a current state and returns None (if no new states can be generated) or Some(Vec<State>) that can be generated from that state
• is_valid - tells if a current state is valid (useful for some cases where I want next_states to generate too many, but I don’t use it for Sudoku)
• is_solved - checks if this state is a solution, if so, we’re done looking

So, let’s implement those for Sudoku:

impl State for Sudoku {
fn is_valid(self) -> bool {
// TODO: Because we're always generating valid next_states
//  this isn't necessary
return true;
}

fn is_solved(self) -> bool {
// TODO: Same as above, all states are is_valid
//  so just check for no remaining empties
for x in 0..9 {
for y in 0..9 {
if self.board[x][y] == 0 {
return false;
}
}
}

return true;
}

fn next_states(self) -> Option<Vec<Sudoku>> {
let mut states = Vec::new();

// Find the next empty square
for x in 0..9 {
for y in 0..9 {
if self.board[x][y] == 0 {
// Try each value
'duplicate: for value in 1..=9 {
for other in 0..9 {
// Already used in this row or column, skip
if self.board[x][other] == value {
continue 'duplicate;
}

if self.board[other][y] == value {
continue 'duplicate;
}

// Already used in this 3x3 block, skip
if self.board[x / 3 * 3 + other / 3][y / 3 * 3 + other % 3] == value {
continue 'duplicate;
}
}

// Valid so far, so generate a new board using that value
let mut next = self.clone();
next.board[x][y] = value;
states.push(next);
}

// Return the possible next states for this empty square
// If we didn't generate any states, something went wrong
if states.len() == 0 {
return None;
} else {
return Some(states);
}
}
}
}

// If we made it here, there are no empty squares, is_solved should be true
// (We shouldn't make it here)
None
}
}

As I mentioned, we’re just skipping is_valid and always returning true, since our next_states function explicitly only returns possible states. Likewise, is_solved just checks if there are any 0s left, since we’re assuming all states are valid.

The interesting one is next_states. For this, we’ll find the next open (0) spot on the board and try each of the 9 possible values. For each, check the row, column, and block it’s in for any duplicates. If there are no duplicates, this will be a state we return. If there are any, skip this one and go on. If we get to the end of this check and none of the values fit into this empty square, this isn’t a valid solution, so return None from next_states. The solver will know how to handle that.

And that’s all we need:

fn main() {
let initial_state = Sudoku {
board: [
[0, 0, 0, 2, 6, 0, 7, 0, 1],
[6, 8, 0, 0, 7, 0, 0, 9, 0],
[1, 9, 0, 0, 0, 4, 5, 0, 0],
[8, 2, 0, 1, 0, 0, 0, 4, 0],
[0, 0, 4, 6, 0, 2, 9, 0, 0],
[0, 5, 0, 0, 0, 3, 0, 2, 8],
[0, 0, 9, 3, 0, 0, 0, 7, 4],
[0, 4, 0, 0, 5, 0, 0, 3, 6],
[7, 0, 3, 0, 1, 8, 0, 0, 0]
]
};
println!("initial {}", initial_state);

for state in initial_state.next_states().unwrap() {
println!("potential {}", state);
}
}

/* --- OUTPUT --- */
initial sudoku:
|26 |7 1
68 | 7 | 9
19 |  4|5
---+---+---
82 |1  | 4
4|6 2|9
5 |  3| 28
---+---+---
9|3  | 74
4 | 5 | 36
7 3| 18|

potential sudoku:
3  |26 |7 1
68 | 7 | 9
19 |  4|5
---+---+---
82 |1  | 4
4|6 2|9
5 |  3| 28
---+---+---
9|3  | 74
4 | 5 | 36
7 3| 18|

potential sudoku:
4  |26 |7 1
68 | 7 | 9
19 |  4|5
---+---+---
82 |1  | 4
4|6 2|9
5 |  3| 28
---+---+---
9|3  | 74
4 | 5 | 36
7 3| 18|

potential sudoku:
5  |26 |7 1
68 | 7 | 9
19 |  4|5
---+---+---
82 |1  | 4
4|6 2|9
5 |  3| 28
---+---+---
9|3  | 74
4 | 5 | 36
7 3| 18|

If you go through it, 3, 4, and 5 are the possible top left states, so those are the ones it generated. In theory, you could optimize slightly by finding the most constrained squares and doing those first, but in practice, this works fine.

Now, on to the actual solver!

## Solving the problem

For what it does, the state is pretty short:

fn solve<S>(initial_state: &S) -> Option<S> where S: State + Copy + std::fmt::Debug {
let mut deq: VecDeque<S> = VecDeque::from([initial_state.clone()]);

while !deq.is_empty() {
let current_state = deq.pop_back().unwrap();

if current_state.is_solved() {
return Some(current_state);
}

// If we have next states, push those onto the queue
// If not, just drop this state (and effectively backtrack)
match current_state.next_states() {
Some(ls) => {
for next_state in ls {
if (next_state.is_valid()) {
deq.push_back(next_state);
}
}
},
None => {}
}
}

return None;
}

Initialize a deque (for the future when I want to support both depth and breadth first searches, a normal Vec would have worked for this) with the initial state then start iterating:

• For each state:
• Check if it’s solved, if so, return that as the answer
• Otherwise, generate each of the possible next_states:
• If that state is valid, add it to the queue
• Otherwise, ignore it
• Because the state is removed, if it has no possible child states, we will automatically backtrack here

Eventually, this will search the entire search space. Because it’s a depth first search, it will go as far down each possible solution branch as it can until it either hits a dead end or finds the solution.

Optimizations:

• Allow either depth or breadth first search
• Keep track of the steps we took to get to a specific state (possibly returning a Vec of tuples of (Step, State))
• Keep track of how many states we evaluated to get to a specific point
• Don’t examine duplicate states (we’ll have to implement Eq for that)

Next time!

## Output time!

And of course it works (and fast), but let’s take a quick look:

fn main() {
let initial_state = Sudoku {
board: [
[0,0,0,0,8,6,0,2,0],
[0,0,6,4,0,0,0,0,0],
[5,0,3,0,0,0,0,0,0],
[0,0,4,6,0,0,7,0,8],
[7,0,0,1,0,0,4,9,0],
[0,0,0,3,0,0,5,0,0],
[0,0,0,8,0,0,2,7,0],
[6,0,0,2,0,3,1,5,0],
[2,0,0,0,9,1,0,0,0],
]
};
println!("initial {}", initial_state);
println!("solved {}", solve::<Sudoku>(&initial_state).unwrap());
}

/* --- OUTPUT --- */

initial sudoku:
|26 |7 1
68 | 7 | 9
19 |  4|5
---+---+---
82 |1  | 4
4|6 2|9
5 |  3| 28
---+---+---
9|3  | 74
4 | 5 | 36
7 3| 18|

solved sudoku:
435|269|781
682|571|493
197|834|562
---+---+---
826|195|347
374|682|915
951|743|628
---+---+---
519|326|874
248|957|136
763|418|259

Nice!


text:
## unity – How to make Player consistently jump *to* a specific target rather than *towards* it?

I’m trying to make it so if my player hits “E” then they jump precisely to a specific target. The current code results in player jumping towards the target but not really making it there.

I’ve tried adjusting forceMultiply and ForceMode and adding an offset but I just can’t get a result that simply consistently launches the player’s rigidbody `rb` towards the `anchorPoint` position.

The code I have is:

``````private void Update()
{
if (Input.GetKeyDown(KeyCode.E))
{
tryGrabbing = true;
}
}

private void FixedUpdate()
{
if (tryGrabbing)
{
}
}
``````

Thank you for any help!!

## physics – (Unity 3D) How to make Player consistently jump *to* a specific target rather than *towards* it?

I’m trying to make it so if my player hits “E” then they jump precisely to a specific target. The current code results in player jumping towards the target but not really making it there.

I’ve tried adjusting forceMultiply and ForceMode and adding an offset but I just can’t get a result that simply consistently launches the player’s rigidbody `rb` towards the `anchorPoint` position.

The code I have is:

``````private void Update()
{
if (Input.GetKeyDown(KeyCode.E))
{
tryGrabbing = true;
}
}

private void FixedUpdate()
{
if (tryGrabbing)
{
}
}
``````

Thank you for any help!!

## bash – Use specific key to connect to jump host without modifying ssh config file

I’m trying to write a script that connect to a linux server by using an other one as a ProxyJump:

``````ssh -J root@proxyhost root@target
``````

I have two different keys (actually ssh certificate) and I would like to tell ssh to use one for the proxy host and the other for the target. I know I could modify the ssh config for that but I would like to specify it on the command line so I don’t have to rely on a valid ssh configuration.

So I’m looking for something like:

``````ssh -i proxyhostkey -J root@proxyhost -i targetkey root@target
``````

The ssh man page of the `-J` options says (emphasis mine):

Note that configuration directives supplied on the command-line
generally apply to the destination host and not any specified jump
hosts. Use ~/.ssh/config to specify configuration for jump hosts.

Is it possible to do want I want ? Or do I have to ensure that the `~/.ssh/config` file will be correct ?

## The Problem

I am using a Logitech K480 Bluetooth keyboard with a 7th generation iPad (iPadOS 14.6) and I often notice that when I am navigating a body of text I have typed (e.g. in the Notes or Facebook apps) with the keyboard arrows the cursor will jump to the beginning of a text field if I push the up arrow twice in a particular location. It can be quite annoying when trying to navigate text I’ve typed; it’s difficult to intentionally navigate using it (or avoid it) because of the variable length of lines in paragraphs.

The first push of the up arrow will move the cursor one line up and then the second push will jump the cursor; it happens both immediately and if I wait. If I push the down key after the jump (again either immediately or if I wait), the cursor will jump back to the original line (i.e. the line I was on before I pushed the up key the first time). The cursor jumping behaviour will occur again in the same manner when pushing the up key twice.

This behaviour consistently occurs if the cursor is at the end of a line following the first up arrow push, no matter the location of the paragraph on the page or the position of the line in the paragraph.

## Related Behaviour

There is some related behaviour. When using Command + left arrow to skip to the end of the line, pushing the up arrow will consistently not move the cursor to the line above but will instead jump the cursor to the beginning of the same line (pushing the down cursor subsequently will jump the cursor back to its original position at the end of the line). Sometimes when navigating a typed document with the arrow keys, a push of the up or down arrow key seems to move two lines at once.

## Possible Explanations

Together these behaviours and their consistency make me think this is an iPadOS ‘autoscrolling’ function, analogous to how deleting text with the onscreen keyboard speeds up the longer the backspace button is held. However, I have not found any documentation of this behaviour by Apple or anywhere else online.

I don’t think this is a feature of the K480 keyboard; it is not listed anywhere in the Logitech documentation, and the responder to my enquiry to Logitech seemed to have no knowledge of this phenomenon (though it was a particularly unhelpful response…). My work’s IT manager thinks it is likely an iPad software feature.

Perhaps this is just a feature of Apple devices that I’m not aware of (e.g. something that’s shared between Macs and iOS devices), but it is strange that I can’t seem to find even a mention of this behaviour.

## The Questions

Has anyone else observed this behaviour? Can it be customised or toggled? Is there some documentation (or personal experience) of the behaviour that lays out how it works?

## unity – How to stop a jump midair and remove y velocity in the process

What I want to do is to cut a jump midair by turning off the y velocity when the player releases the jump button (like in Hollow Knight). I managed to do that with:

``````rb.velocity = new Vector2(rb.velocity.x, 0f);
``````

My problem is when I cut the jump and I am midair, if I repeat the release jump button process, the whole thing happens again, the character staggers as long as I am releasing the jump button continously.

I would like to be able to do that only once when I am off the ground. I am a noob when it comes to coding so I don’t really know what to do.

`````` using System.Collections;
using System.Collections.Generic;
using UnityEngine;
using UnityEngine.Events;

public class PlayerController : MonoBehaviour {

public Animator animator;

private Rigidbody2D rb;
public float speed;
private float moveInput;
public float jumpForce;

private bool isGrounded;
public Transform feetPos;

private float jumpTimeCounter;
public float jumpTime;
private bool isJumping;
private bool facingRight = true;
public float jumpDownForceY = 0;

void Start()
{
rb = GetComponent<Rigidbody2D>();

}

void Update()
{

if (Input.GetButtonDown("Jump") && rb.velocity.y == 0)

if (Mathf.Abs(moveInput) > 0 && rb.velocity.y == 0)
animator.SetBool("Running", true);
else
animator.SetBool("Running", false);

if (rb.velocity.y == 0)
{
animator.SetBool("Jumping", false);
animator.SetBool("Falling", false);
}

if (rb.velocity.y > 0.2)
{
animator.SetBool("Jumping", true);
}

if (rb.velocity.y < 0)
{
animator.SetBool("Jumping", false);
animator.SetBool("Falling", true);
}

if (isGrounded == true && Input.GetButtonDown("Jump"))
{
isJumping = true;

jumpTimeCounter = jumpTime;
rb.velocity = Vector2.up * jumpForce;
}

if (Input.GetButton("Jump") && isJumping == true)
{

if (jumpTimeCounter > 0){
rb.velocity = Vector2.up * jumpForce;
jumpTimeCounter -= Time.deltaTime;
} else {
isJumping = false;
}

}

if (Input.GetButtonUp("Jump"))
{
isJumping = false;
rb.velocity = new Vector2(rb.velocity.x, 0f);

}

}

void FixedUpdate()
{
moveInput = Input.GetAxisRaw("Horizontal");
rb.velocity = new Vector2(moveInput * speed, rb.velocity.y);
Flip(moveInput);

}

private void Flip(float moveInput)
{
if (moveInput > 0 && !facingRight || moveInput < 0 && facingRight)
{
facingRight = !facingRight;
Vector3 theScale = transform.localScale;
theScale.x *= -1;
transform.localScale = theScale;
}

}
}
``````

## libgdx – Should delta be applied to every change per frame ? (e.g. acceleration, deceleration, jump, etc.?)

I have written a game based on another game’s original physics. I have all the constants the original game used in the Sega Megadrive. For example:

``````float ACCELERATION = 0.03287f;
float DECELERATION = 0.4f;
float FRICTION     = ACCELERATION;
float TOP_SPEED    = 8f;
``````

when the player presses the right button I do:

``````     if (rightPressed) {
speed.x += ACCELERATION * delta; // accelerate

if (speed.x >= TOP_SPEED * delta) {
speed.x = TOP_SPEED * delta; // impose a top speed limit
}
}
...
else { // user is not moving the player (left/right)
speed.x -= Math.min(Math.abs(speed.x), FRICTION * delta) * Math.signum(speed.x);
}
``````

Several lines later:

``````    x += speed.x * delta;
y += speed.y * delta ;

``````

Is the delta here used correctly? Should it appear anywhere as I did or just the moment I set x and y? My understanding is that speed should accelerate according to delta as well.

Another problem I have is that, by using the original game constants, the character moves in slow motion (even if I only have delta at the moment of updating x and y) so I had to multiply all constants by 15000 in order to have normal playing speed. I expected I may have to multiply by 60 (because of the 60 frames per second of Sega Megadrive) but not by 15000.

## c++ – SFML – My jump never stops

Im making a short jump test in sfml. However I have a problem, whenever the jump button is pressed the character will jump but will not fall down, he will keep going higher. However, in the beginning of the test, I made the sprite above the ground to see if the gravity function worked, but this still happens. Here is a video

Here is my code:

``````#include <SFML/Graphics.hpp>
using namespace sf;

float VelocityX = 0, VelocityY = 0;
float x = 0, y = 0;
int gravity = 2;
float dt;

void movement() {
if (y < 444) {
VelocityY += gravity * dt;
}
else if (y > 444) {
y = 444;
}
x += VelocityX;
y += VelocityY;
}

int main() {
RenderWindow window(VideoMode(800, 600), "jump test");
RectangleShape rect(Vector2f(20, 20));
const int moveSpeed = 500, jumpForce = 10;

Clock deltaTime;
while (window.isOpen())
{
dt = deltaTime.restart().asSeconds();
Event event;

while (window.pollEvent(event)) {
if (event.type == Event::Closed) {
window.close();
}
}

if (Keyboard::isKeyPressed(Keyboard::Right)) {
VelocityX = moveSpeed * dt;
}
else if (Keyboard::isKeyPressed(Keyboard::Left)) {
VelocityX = -moveSpeed * dt;
}
else {
VelocityX = 0;
}

if (Keyboard::isKeyPressed(Keyboard::Space)) {
VelocityY -= jumpForce;
}

movement();
rect.setPosition(x, y);

window.clear();
window.draw(rect);
window.display();
}

return 0;
}
$$```$$
``````

I am trying to create a google sheet that lists all payments made for tuition by family. I would like to use only one tab (not create a tab for each family) as I have about 120 families to keep track of.

Any thoughts of the best way to do this without having to scroll forever to get to the specific family I need to look at? Currently I have the families listed in alphabetical order in multiples of 4 going down and then the next set of 4, etc. This is easier when it comes to printing certain sections of the sheet for cross reference (ie not having to scroll down forever to find a name).

Date Family
Penland
8/6/20 \$150 cc = app fee
8/17/20 \$550 ck #2635 = reg, corp
9/10/20 \$650 ck #3016 = Aug tuit
10/12/20 \$650 ck #4361 = Oct tuit
11/10/20 \$650 ck #3027 = Nov tuit
12/16/20 \$650 ck #2143 = Dec tuit
1/20/21 \$650 ck #2738 = Jan tuit
2/26/21 \$650 ck #4622 = Feb tuit

I know how to use the F5 shortcut to get to a specific cell but how do you get to a specific cell by typing in the name of the family? That would help with the whole scrolling issue.

Or if anyone has a better idea of how to record these payments I’d love your help.

## plugins – Shortcode use creates a scroll error/ jump to top of page?

plugins – Shortcode use creates a scroll error/ jump to top of page? – WordPress Development Stack Exchange


text:
Building MVC structure with PHP

For Web Security class we had to write a web application and secure it in any preferred language. Since PHP was showcased and introduced in all of the demos throughout the class, we decided to stick with it for the sake of simplicity. Furthermore, we also set the goal of building a proper MVC sturcture just to give ourselves some extra challenge.

In this tutorial I am going to write about the project’s structure, touch upon the .htaccess file and talk about some apache configurations.

Structure of the project

The main idea behind the architecture was that we wanted to access everything through index.php and forbid direct accessibility of any other files and folders.

- config/
- modules/
- helpers/
- services/
- css/
- libs/
- index.php
- .htaccess

We will access our configuration files from config/ folder, such as database credentials, file paths or translation files, which have to be available throughout the entire application.

Modules will be a group of controllers and views, for example a Login module will have a LoginController and a LoginView. They will be responsible for handling the requests, processing data, and exposing data for the users.

Modules may use some Helper classes to use commonly used independent methods throughout the application (for example building links with a LinkBuilder, or authenticate the user with an Authenticator).

Module controllers will rely on Services to fetch data from the database. Only services will include SQL code. On any given parameters they will try to get the desired data and return it to the controller.

Of course, we will have separate folders for our CSS codebase and for our external libraries.

Every request will call index.php with some custom parameters, so everything will be centralized and will be under controll. Based on the inputs, an included router.php will handle the routing for us. But how do we force every traffic to go to index.php? We will use the .htaccess file.

Configuring .htaccess

What is .htaccess at all? From http://www.htaccess-guide.com:

.htaccess is a configuration file for use on web servers running the Apache Web Server software. When a .htaccess file is placed in a directory which is in turn ‘loaded via the Apache Web Server’, then the .htaccess file is detected and executed by the Apache Web Server software. These .htaccess files can be used to alter the configuration of the Apache Web Server software to enable/disable additional functionality and features that the Apache Web Server software has to offer.

In order to make this configuration file work, we might have to change our apache settings in our apache.conf, which is located under /etc/apache2/apache2.conf in Ubuntu. Change AllowOverride from none to All like so:

 <Directory /var/www/>

AllowOverride All

</Directory>

We need one more thing; we have to activate the mod_rewrite module on Apache. To do so, we have to use the following command:

sudo a2enmod rewrite

After that, don’t forget to restart Apache:

sudo service apache2 restart

Now we can apply our own rules to handle requests coming to our Apache server.

.htaccess file

Let’s rewrite some rules.

# Disable directory listing
Options -Indexes

# URL Rewrite
RewriteEngine on
RewriteRule ^(modules/|common/|config/|helpers/|services/) - [F,L,NC]
RewriteRule ^([^/.]+)/?$index.php?controller=$1&action=index
RewriteRule ^([^/.]+)/([^/.]+)/?$index.php?controller=$1&action=$2 RewriteRule ^([^/.]+)/([^/.]+)/([^/.]+)/?$ index.php?controller=$1&action=$2&parameter=$3  First, the Options -Indexes line disables directory listing, so our files will not be listed when we request a folder without index.php or index.html on the server. Then, we turn on the RewriteEngine, so we can set up our rules. Our first rule is about forbidding direct access to certain folders. This way the contents of those folders won’t be accessable outside of localhost - only index.php will be able to require or include anything from these sources, any requests coming from different domains will be rejected. The next few lines will translate RESTFUL API-like URIs into the language of our index.php using regex. So, for example posts/edit/3 will be translated into index.php?controller=posts&action=edit&id=3. At this point, we should not be able to access the mentioned folders, and when navigating to libs or css we should not get any lists of content - if that’s the case, we are good to go. config/config.php We will store a couple of our configurations in a config.php file, so we can avoid (or reduce so to speak) using hard coded values. <?php // Default module const DEFAULT_CONTROLLER = "Home" const DEFAULT_ACTION = "Dashboard" // Server configurations const SERVER_NAME = "localhost"; const DB_USERNAME = "root"; const DB_PASSWORD = ""; const DB_NAME = "dbname"; ?>  index.php <?php require_once('config/config.php');$controller = DEFAULT_CONTROLLER;
$action = DEFAULT_ACTION;$parameter = null;

if (isset($_GET['controller']) && isset($_GET['action']))
{
$controller = strtolower($_GET['controller']);
$action = strtolower($_GET['action']);
$parameter = isset($_GET['parameter']) ? strtolower($_GET['parameter']) : null } ?> <!DOCTYPE html>   <meta charset="UTF-8"> <meta name="viewport" content="width=device-width, initial-scale=1.0"> <title>My site</title> <link rel="stylesheet" href="css/style.css">   <?php include_once("config/router.php"); ?>    After loading up our configuration file, we are going to set up a default controller and a default action right away. If no controller and action will be defined as parameters, we are going to use these defaults, otherwise we define the setup as requested. An action parameter is often times optional or not required at all, so we build the requirements accordingly. In the document body we are going to fire off the router, which will initiate the requested controller and trigger its action. config/router.php <?php function callAction($controller, $action,$parameter)
{
switch ($controller) { case "home": require_once("modules/HomeModule/HomeController");$controller = new HomeController();
break;
case "profile":
require_once("modules/ProfileModule/ProfileController");
$controller = new ProfileController(); break; default: pageNotFound(); } if (!method_exists($controller, $action)) { pageNotFound(); } if ($parameter)
{
$controller-> {$action }($parameter); } else {$controller-> { $action }(); } } function pageNotFound() { // require_once("modules/HomeModule/HomeController"); //$controller = new HomeController();
// $controller->dashboard(); echo "404 - Page not found"; } callAction($controller, $action,$parameter);
?>

This file contains two simple methods: callAction, which will try to call the requested action, and pageNotFound, which will get called when something goes wrong when preparing the controller and its action. We can handle pageNotFound any way we wish; we can redirect the user if we want using the header() method, we can initiate any desired controller and kick-off one of its actions, or we can just simply echo an error message.

One thing to mention: instead of a switch-case statement, we could simply construct the location path string based on the controller name. However in that case we would have to check whether the requested file exists or not with file_exists(), which infers further security issues. Switch-case however has a white-listing approach where only accepted strings will execute further code.

Our router is ready, if we try to access a controller named other than home or profile (for example if our application is located at localhost then by calling localhost/posts or localhost/index.php?controller=posts), we should get our 404 page.

However a site with only a 404 page is not much of a fun, so let’s create our HomeController class.

modules/HomeModule/HomeController.php

<?php
class HomeController
{
private $breadcrumbs; private$view;

public function __construct()
{
$this->breadcrumbs = "HomeController";$this->view = "modules/HomeModule/HomeView.php";
}

public function dashboard()
{
$breadcrumbs =$this->breadcrumbs + " / Dashboard";
require_once($this->view); } public function inbox() {$breadcrumbs = $this->breadcrumbs + " / Inbox"; require_once($this->view);
}

}
?>

Our HomeController will have two properties: some kind of data which we are going to process, and a view to expose it to the user. In the constructor we are assigning values to these properties: the data we will process is a simple breadcrumbs navigation. So our private property will hold the string HomeController by default, and we are going to concatenate further strings based on the action called by the user. After this tiny operation, we are going to reveal the result to the user through a view.

modules/HomeModule/HomeView.php

<?php echo $breadcrumbs; ?>

Hello baby, don't say maybe!

  Now let’s test this. If everything went well, assuming that our index.php is located in the root of localhost, we can access our methods at localhost/home/dashboard and localhost/home/inbox. Services So far we have the View and Controller part of the MVC structure. Let’s take care of the Model in the shape of services. A service will be initialised with a database context. It will try to use this context to fetch the data from, and will always return the result, so the controller can do the error-handling. Let’s create a post service, which will be used to fetch all posts written by the users, or to retrieve one post fetched by its ID. <?php class PostService { private$db;
function __construct($dbConnection) {$this->db = $dbConnection; } public function getPosts() {$sql = "SELECT * FROM POSTS";
$stmt =$this->db->prepare($sql); if (!$stmt->execute())
{
return false;
}

$table =$stmt->get_result();
return mysql_fetch_array($table, MYSQL_ASSOC); } public function getPostById($postId)
{
$sql = "SELECT * FROM POSTS WHERE ID = ?";$stmt = $this->db->prepare($sql);
$stmt->bind_param('i',$postId);
if (!$stmt->execute()) { return false; }$table = $stmt->get_result(); return mysqli_fetch_object($table);
}
}
?>

As we can see, this class needs a DbContext to be initialised with. Both of its methods return false if the script execution fails; otherwise they will return the result of the query.

At this point this class is on its own, it is not included anywhere. We have 2 final things to do to connect the dots: first we have to create a database connection, which we can pass to the PostService, and then we have to include the PostService in our HomeController.

helpers/DbContext.php

<?php
class DbContext
{
private $servername = SERVER_NAME; private$username = DB_USERNAME;
private $password = DB_PASSWORD; private$dbName = DB_NAME;
public $dbConnection; public function __construct(){$this->dbConnection = new mysqli(
$this->servername,$this->username,
$this->password,$this->dbName
);
}
}
?>

That’s it! Now, after including this helper class to our controller, we can easily initialise a database context by doing $db = new dbContext(), and we will be able to access its connection by $db->dbConnection. After creating our service with this helper, we will utilize the service to obtain and expose data to the users.

Our new HomeController.php will be:

<?php

require_once("helpers/DbContext.php");
require_once("services/PostService.php");

class HomeController
{
private $breadcrumbs; private$view;
private $PostService; public function __construct() {$db = new DbContext();
$dbConnection =$db->dbConnection;
$this->PostService = new PostService($dbConnection);
$this->breadcrumbs = "HomeController";$this->view = "modules/HomeModule/HomeView.php";
}

public function dashboard()
{
$breadcrumbs =$this->breadcrumbs + " / Dashboard";
$posts =$this->PostService->getPosts();
require_once($this->view); } public function inbox() {$breadcrumbs = $this->breadcrumbs + " / Inbox";$posts = $this->PostService->getPostById(1); require_once($this->view);
}

}
?>

First we include our dependencies on the top, so we can use our DbContext and PostService classes. Then, in the constructor we intialise one instance of the DbContext and then, using its dbConnection property, we create our PostService instance, which is going to be a property of our HomeController.

Now, we can use this service in our controller, to get the desired data, by doing e.g.: $posts =$this->PostService->getPosts();.

All we have left to do is to reveal our data in our view:

<?php echo $breadcrumbs; ?>   <?php if ($posts): ?>

<?php var_dump($posts); ?>
 <?php endif; ?>  <?php if ($post): ?>

<?php var_dump(\$post); ?>

<?php endif; ?>

This way we managed to create a solid foundation for our application, which fulfills the separation of concerns princible by dividing our Modules into Views and Controllers and by having an isolated block for our Models in the shape of services.


text:
Definitions

# GDP deflator

In economics, the GDP deflator (implicit price deflator for GDP) is a measure of the change in prices of all new, domestically produced, final goods and services in an economy. GDP stands for gross domestic product, the total value of all final goods and services produced within that economy during a specified period.

## Calculation

### Measurement in national accounts

In most systems of national accounts the GDP deflator measures the difference between the real (or chain volume measure) GDP and the nominal (or current price) GDP. The formula used to calculate the deflator is:

$operatorname\left\{GDP deflator\right\} = frac\left\{operatorname\left\{Nominal GDP\right\}\right\}\left\{operatorname\left\{Real GDP\right\}\right\}times 100$

Dividing the nominal GDP by the GDP deflator and multiplying it by 100 would then give the figure for real GDP, hence deflating the nominal GDP into a real measure.

It is often useful to consider implicit price deflators for certain subcategories of GDP, such as computer hardware. In this case, it is useful to think of the price deflator as the ratio of the current-year price of a good to its price in some base year. The price in the base year is normalized to 100. For example, for computer hardware, we could define a "unit" to be a computer with a specific level of processing power, memory, hard drive space and so on. A price deflator of 200 means that the current-year price of this computing power is twice its base-year price - price inflation. A price deflator of 50 means that the current-year price is half the base year price - price deflation.

Unlike some price indexes, the GDP deflator is not based on a fixed basket of goods and services. The basket is allowed to change with people's consumption and investment patterns. (Specifically, for GDP, the "basket" in each year is the set of all goods that were produced domestically, weighted by the market value of the total consumption of each good.) Therefore, new expenditure patterns are allowed to show up in the deflator as people respond to changing prices. The advantage of this approach is that the GDP deflator reflects up to date expenditure patterns. For instance, if the price of chicken increases relative to the price of beef, people would likely spend more money on beef as a substitute for chicken. A fixed market basket measurement would miss this change.

In practice, the difference between the deflator and a price index like the CPI is often relatively small. On the other hand, with governments in developed countries increasingly utilizing price indexes for everything from fiscal and monetary planning to payments to social program recipients, the even small differences between inflation measures can shift budget revenues and expenses by millions or billions of dollars.

### United States

The GDP and GDP deflator are calculated by the Bureau of Economic Analysis (BEA).

### United Kingdom

The GDP and GDP deflator series are published by the Office for National Statistics.

## Hedonics

A hedonic regression for a specific good relates the expected price of the good to its characteristics. For example, a hedonic model for a computer relates a computer's price to the value of its processor speed, memory, hard drive capacity, and so on. Hedonic regressions can be used to create hedonic price indexes. These can vary over time as the price structure of the underlying characteristics change.

In recent years, some commentators have expressed concern that the national accounts may overstate spending on computer hardware because of the way the hedonic index and implicit price deflator are used. It is well-known that the prices of a unit of processor speed, a unit of memory, and a unit of hard drive capacity have declined very quickly since 1995. Therefore, the current-year (say, 2003) price deflator for an entire computer - using the hedonic method - is less than one relative to a base year of 1995. This means that when nominal spending on computer hardware is divided by the deflator to give real spending on computers, the number rises. (The "deflator" here is actually an inflator!) From the second quarter of 2000 through the fourth quarter of 2003, the government estimated that real tech spending rose from \$446 billion to \$557 billion, when nominal spending only increased to \$488 billion. Some analysts feel that this overstates the "true" spending on computers by \$72 billion. However, it is also true that this extra \$72 billion captures the increase in value and utility of the computers that were purchased in 2003 as compared to 2000, due to the former's superior quality and capability for the same nominal price as the latter.

## References

### Hedonics

Search another word or see Implicit price deflatoron Dictionary | Thesaurus |Spanish


text:
#### Enclave-Aware Compartmentalization and Secure Sharing with Sirius

Hardware-assisted trusted execution environments (TEEs) are critical building blocks of many modern applications. However, they have a one-way isolation model that introduces a semantic gap between a TEE and its outside world. This lack of information causes an ever-increasing set of attacks on TEE-enabled applications that exploit various insecure interactions with the host OSs, applications, or other enclaves. We introduce Sirius, the first compartmentalization framework that achieves strong isolation and secure sharing in TEE-assisted applications by controlling the dataflows within primary kernel objects (e.g. threads, processes, address spaces, files, sockets, pipes) in both the secure and normal worlds. Sirius replaces ad-hoc interactions in current TEE systems with a principled approach that adds strong inter- and intra-address space isolation and effectively eliminates a wide range of attacks. We evaluate Sirius on ARM platforms and find that it is lightweight ($\approx 15K$ LoC) and only adds $\approx 10.8\%$ overhead to enable TEE support on applications such as httpd, and improves the performance of existing TEE-enabled applications such as the Darknet ML framework and ARM's LibDDSSec by $0.05\%-5.6\%$.


text:
# Finding statistical significant difference between multiple linear regressions (in R)? [duplicate]

I have a faceted graph, and I want to be able to test whether or not the slope of one regression line in one of the division is significantly different from both a) the other lines within its facet, and b) the line of the same grouping in the other facet.

Basically, I want to be able to test whether, for example, the red 'X' regression line in the 'A' facet is statistically different from the green 'Y' line and the blue 'Z' line within its own facet, and, more importantly, statistically different from the red 'X' line in the 'B' facet.

The graph was produced from this data in R...

ex.ID <- c(1,1,1,1,1,2,2,2,2,2,3,3,3,3,3,4,4,4,4,4,5,5,5,5,5,6,6,6,6,6,7,7,7,7,7,8,8,8,8,8,9,9,9,9,9,10,10,10,10,10,11,11,11,11,11,12,12,12,12,12)
ex.month <- c(0,6,12,18,24,0,6,12,18,24,0,6,12,18,24,0,6,12,18,24,0,6,12,18,24,0,6,12,18,24,0,6,12,18,24,0,6,12,18,24,0,6,12,18,24,0,6,12,18,24,0,6,12,18,24,0,6,12,18,24)
ex.label <- c("A","A","A","A","A","B","B","B","B","B","B","B","B","B","B","A","A","A","A","A","A","A","A","A","A","B","B","B","B","B","B","B","B","B","B","A","A","A","A","A","B","B","B","B","B","A","A","A","A","A","B","B","B","B","B","A","A","A","A","A")
ex.score <- c(100,100,89,85,70,95,90,90,86,80,84,80,71,68,60,100,100,98,90,92,100,95,90,85,80,98,96,90,83,81,85,80,78,72,69,95,90,89,85,80,90,84,83,80,75,90,80,80,77,75,91,90,82,76,73,93,90,84,80,75)
ex.status <- c("Y","Y","Y","Y","Y","Z","Z","Z","Z","Z","Y","Y","Y","Y","Y","Y","Y","Y","Y","Y","Z","Z","Z","Z","Z","Z","Z","Z","Z","Z","Y","Y","Y","Y","Y","Z","Z","Z","Z","Z","X","X","X","X","X","X","X","X","X","X","X","X","X","X","X","X","X","X","X","X")

ex.df <- data.frame(ex.ID,ex.month,ex.label,ex.score,ex.status)

I've done some looking around, and some sources suggested that an ANOVA test could be capable of accomplishing what I need to do. However, I am not entirely sure this is correct, and I thought I would check here. In addition, if that is correct, I have no idea how to actually do that test.

In essence, all I want to do is determine whether two regression lines are significantly different, but in this specific circumstance in R. Thank you.

• The most common approach would be do something like ANCOVA, but because you are comparing several lines, it might be easier to construct 95% confidence intervals about each coefficient, and then conclude that coefficients without any overlap in their confidence intervals are statistically different. You could compare intercepts to intercepts and slopes to slopes. – Sal Mangiafico Jul 20 '17 at 21:56
• ANCOVA with post-hoc tests should serve you well: stats.stackexchange.com/a/2472/121522 – mkt - Reinstate Monica Jul 21 '17 at 14:42


text:
## Wikipedia - Grado Celsius Celsius temperature, $$t$$, $$\theta$$

https://doi.org/10.1351/goldbook.C00928
@T06321@ minus $$273.15\ \text{K}$$, invariably expressed in the SI unit @D01561@ ($$^{\unicode{x26ac}}\text{C}$$) which is equal to the @K03374@. Sometimes the misnomer centigrade temperature is used for Celsius temperature.
Sources:
Green Book, 2nd ed., p. 48 [Terms] [Book]
PAC, 1996, 68, 957. (Glossary of terms in quantities and units in Clinical Chemistry (IUPAC-IFCC Recommendations 1996)) on page 965 [Terms] [Paper]


text:
# Statements of conjectures

## Donovan's conjecture

Donovan's conjecture can be stated over a field or a complete discrete valuation ring. It is usual to assume the field is algebraically closed, and it is no loss to assume it is the algebraic closure $k$ of the field with $p$ elements, as in the notation section.

### $k$-Donovan conjecture

Let $P$ be a finite $p$-group. Then there are only finitely many possible Morita equivalence classes for blocks of $kG$ for finite groups G with defect group isomorphic to $P$.

The situation with choice of discrete valuation ring is a little more complicated, as discussed in the notation section, and we take $\mathcal{O}$ to be the ring of Witt vectors for $k$.

### $\mathcal{O}$-Donovan conjecture

Let $P$ be a finite $p$-group. Then there are only finitely many possible Morita equivalence classes for blocks of $\mathcal{O} G$ for finite groups G with defect group isomorphic to $P$.

## Weak Donovan conjecture

This arose as a question of Brauer (where he asked whether the Cartan invariants (the entries of the Cartan matrix) are bounded by the order of a defect group). The answer to Brauer's precise question is no, but Donovan asked the more general question:

### Weak Donovan conjecture

Let $P$ be a finite $p$-group. Then there is $c=c(P) \in \mathbb{N}$ such that for all blocks of $kG$ for finite groups G with defect group isomorphic to $P$, the Cartan invariants are at most $c$.

By [Du04, pp. 19] the weak Donovan conjecture is equivalent to the following two conjectures together.

### Loewy length conjecture

Let $P$ be a finite $p$-group. Then there is $l=l(P) \in \mathbb{N}$ such that for all blocks of $kG$ for finite groups G with defect group isomorphic to $P$, the Loewy length is at most $l$.

### Ext space conjecture

Let $P$ be a finite $p$-group. Then there is $e=e(P) \in \mathbb{N}$ such that for all blocks $B$ of $kG$ for finite groups G with defect group isomorphic to $P$ and for all pairs $V, W$ of simple $B$-modules, $\dim_k({\rm Ext}_{kG}^1(V,W)) \leq e$

## Morita-Frobenius number conjectures

In [Ke05] Kessar showed that the $k$-Donovan conjecture is equivalent to the Weak Donovan conjecture together with the following.

### Kessar's conjecture

Let $P$ be a finite $p$-group-group. Then there is $m=m(P) \in \mathbb{N}$ such that if $G$ is a finite group and $B$ is a block of $kG$ with defect groups isomorphic to $P$, then ${\rm mf}_k(B) \leq m$.

This may be reformulated over $\mathcal{O}$. In [EEL18] it is shown that the $\mathcal{O}$-Donovan conjecture is equivalent to the Weak Donovan conjecture together with the following.

### $\mathcal{O}$-Kessar conjecture

Let $P$ be a finite $p$-group-group. Then there is $m=m(P) \in \mathbb{N}$ such that if $G$ is a finite group and $B$ is a block of $\mathcal{O} G$ with defect groups isomorphic to $P$, then ${\rm mf}_\mathcal{O}(B) \leq m$.

This conjecture is considered in an equivalent form in [EL18b] .

## Puig's conjecture

The following conjecture is very natural, but since it is very hard to reduce to quasisimple groups is known in very few cases.

### Puig's conjecture

Let $P$ be a finite $p$-group. Then there are only finitely many possible isomorphism classes source algebras for blocks of $kG$ for finite groups G with defect group isomorphic to $P$.

Here we mean an isomorphism of interior algebras.

## Broué's conjecture

This may be stated in several different forms. The basic version that we take here is:

### Broué's conjecture

Let $G$ be a finite group and $B$ be a block of $\mathcal{O} G$ with abelian defect group $D$. Let $B$ be the unique block of $\mathcal{O} N_G(D)$ with Brauer correspondent $B$. Then $B$ is derived equivalent to $b$.

It is expected that further there should be a splendid derived equivalence, and even that there should be a chain of perverse equivalences (see [CR13]).


text:
# Label does not maintain correct position within a Table

I'm hoping the fix is quite simple, but this has become increasingly frustrating. I've built a minimally reproducable example. This is how the table is rendered:

And this is the corresponding code:

    private Table testTable() {
Table table = new Table();
Skin skin = new Skin(Gdx.files.internal("skin/uiskin.json"));
Label label1 = new Label("String", skin);
Label label2 = new Label("Hello", skin);
Label label3 = new Label("World", skin);

table.add(label1);

table.row();

table.add(label2).width(100).height(100);
table.add(label3).width(200).height(200);

table.setFillParent(true);
table.debugAll();

return table;
}

As you can see, the "Hello" and "World" labels are not centered within their logical tables. Further, even if I try .width(100).height(100).center(), or even .bottom().right(), for example, the two labels' positions are always fixed to the left, center of their logical table.

The only way I could 'fix' the problem is by excluding the .width().height(), but I need them for my UI.

Any thoughts?

## 2 Answers

To understand why left() right() center() etc. doesn't work try doing label1.left() or label2.top(). See how they move to be top / left aligned? Well why is this?

This is because those methods align the Actor inside of the Cell, not the content inside of the Actor. To understand take a look at my (super professional) drawing:

See how label1 and label2 does not occupy the entire cell, but label3 does? This is why we can change the alignment of label1 and label2 but not label3. From this picture we can also see that if we align label1.top() or label2.left() this wouldn't have any effect since they cannot be moved in that direction.

## Solution

If you want to align the text inside of a Label use Label#setAlignment() with one or more constants from the Align class (docs). In your case you need setAlignment(Align.center) to center the text inside of the label.

Code:

private Table testTable() {
Table table = new Table();
Skin skin = new Skin(Gdx.files.internal("skin/uiskin.json"));
Label label1 = new Label("String", skin);
Label label2 = new Label("Hello", skin);
label2.setAlignment(Align.center); // Align
Label label3 = new Label("World", skin);
label3.setAlignment(Align.center); // Align

table.add(label1);

table.row();

table.add(label2).width(100).height(100);
table.add(label3).width(200).height(200);

table.setFillParent(true);
table.debugAll();

return table;
}

This will produce this result:

In your current code you are expanding the actors (in this case labels) themselves by setting .width(xxx) and .height(xxx). You can see this by the green rectangles which indicate your actor. Since the labels are by default aligned to the left your text will show aligned to the left. If you do .right() there will be no change since it's already on the right since it's stretches the whole cell.

One easy fix would be to set the alignment of your labels.

label2.setAlignment(Align.center);
label3.setAlignment(Align.center);

You can add additional alignments by using "|" like label3.setAlignment(Align.center | Align.top);.

I guess you want to be the world as large as possible and the main table to fill the whole screen. This can be done with the expand() and fill() method. This will adjust the size to fill the whole table, you already told the table to fit the stage by setting it to fill it's parent.

private Table testTable() {
Table table = new Table();

Label label1 = new Label("String", skin);
Label label2 = new Label("Hello", skin);
Label label3 = new Label("World", skin);

table.columnDefaults(1).width(300);

table.add(label1).row();

table.add(label2);
table.add(label3).expand().fillX(); //<-- only change

table.setFillParent(true);
table.debugAll();

return table;
}

Since by default widgets/actors are aligned to center within the table cell both label1 and label2 will be centered. If you want to have some extra room in your left column you can also use padding and leave the alignment of text with

table.add(label1).pad(20).row();


text:
# Can you get the inertia from the angular speed?

1. Mar 15, 2017

### Ys VL

1. The problem statement, all variables and given/known data

2. Relevant equations
...

3. The attempt at a solution

I've been searching for the relation between the spinning speed and inertia in equation form. I do know that since the skater inertia is smaller the spinning speed is faster but that about it. Any hint would be helpful. One more thing, is angular velocity and angular speed the same thing?

2. Mar 15, 2017

### Staff: Mentor

Welcome to the PF.

The textbook that you took a picture of should have the relevant equations. Since the skater is spinning only about the vertical axis, the angular speed and the vector angular velocity can be considered to be the same.

What quantity is conserved as the skater pulls her arms in? What is the equation relating that conserved quantity to the moment of inertia (MOI) and her angular speed?

3. Mar 15, 2017

### Ys VL

I'm sorry but my teacher made this up and handed us a to do list. I have no idea where he got it from but I must solve it. To answer directly all I have to work with is what is given in this sentence, the rest is from my knowledge of the class notes.

Last edited: Mar 15, 2017
4. Mar 15, 2017

### haruspex

Do your notes have anything on angular momentum? If not, try g**gling it.

5. Mar 16, 2017

### Ys VL

I'm back,

I looked up angular momentum. From what I can tell if I calculate L (angular momentum) I should have no problem solving this since L is suppose to be constant and the tangential velocity is given for it's final and initial. I tried it and I think I finally got it. If this is right thanks haruspex, if not..... what else do you think I should look up?

Did I do it correctly?

Last edited: Mar 16, 2017
6. Mar 16, 2017

### haruspex

Looks right - but you should always include the units in the answer, or better still at every step in the calculation.