text:
# Machine Learning’s Poor Fit for Real Data

There’s a growing sentiment out there with all the wonderful things happening in artificial intelligence, machine learning, and data science that these technologies are ready to solve all the things (including how to kill all humans). The reality is there are still a bunch of significant hurdles between us and the AI dystopia/utopia. One big one that is the main impetus behind my research is the disconnect between the statistical foundations of machine learning and how real data works.

Machine learning technology is built on a foundation of formal theory. Statistical ideas, computer science algorithms, and information-theoretic concepts integrate to yield practical methods that analyze large, noisy data sets to train actionable and predictive models. The power of these methods has caused many to realize the value of data.

Yet, as data collection accelerates, weaknesses of existing machine learning methods reveal themselves. The nature of larger-scale data collection violates key assumptions in the foundation that made machine learning so effective. Most notably, statistical independence is no longer achievable with large-scale data. Data is being collected from highly interacting, entangled, complex systems. Human data describes people interacting in a single global social network; ecological data represents measurements of organisms inhabiting complex, shared ecosystems; and medical data measures the interconnected, biological systems that govern health.

## Origins in Experimental Statistics

The concept of statistical independence is a natural fit for laboratory experimentation. In laboratory experiments, scientists test hypotheses by running repeated experiments in closed environments. By design, the measurements taken during each experiment are independent. Because one experiment can’t affect another’s result, classical statistics can confidently quantify the effects of factors in the experiment, even in the presence of randomness.

For example, a typical pre-clinical laboratory drug trial would use a population of animal subjects, administering a drug to part of the population and giving no treatment to a separate control subpopulation. The two subpopulations would be managed to ensure that confounding factors, such as genetics, are equally distributed. The individual subjects would be kept separated in isolated environments. By preventing subjects from interacting with each other, any observations of the drug’s effects can be considered fully independent samples, and classical statistics would enable comparison of effects with quickly converging confidence intervals.

In modern data, measurements are taken from “the wild.” Modern data is analogous to a version of the experiment where the animal subjects interact, sharing food, contact, and communication. Generally, data collections describe large populations of interacting parts, with each measurement related through correlated paths. As modern data collection technology becomes faster and cheaper, the data necessarily becomes increasingly interdependent.

Illustration of the data cleaning task. A common view of complex data is that it can be “cleaned” to fit the structure expected in classical statistics and machine learning methods. But this cleaning typically decimates the nuanced information present in data from real-world, complex phenomena.

## The Myth of Clean Data

It’s tempting to interpret these nuances of real-world data to be simply nuisances. One may attempt to convince oneself that the discrepancy between classical statistical methods and real data can be remedied by data cleaning. Data cleaning—a key skill in modern data analysis—involves taking raw data, processing it to remove spurious outliers, undesired dependencies, and biases created by interacting measurements, then performing supposedly clean analysis on the supposedly clean data.

The clean data concept encourages deliberate omission of information, introduction of unjustified assumptions, and fabrication of facts, to turn real-world data, with all its complexities, into rectangular tables of independent samples. These manipulations undo many of the virtues of data-driven thinking.

The perception that machine learning methods require such destructive preprocessing is a major failure in the technology transfer from machine learning research to practical application. And the reasons for this failure manifest in the various costs associated with more nuanced machine learning methods. Methods that can reason about interdependent data require more computational cost—the amount of computer time and energy needed to learn, reason, and predict using these methods—and cognitive cost—the amount of expertise necessary to apply, understand, and interpret these methods.

## “Conclusion”

So what’s the point of my arguments here? I’m not super certain, but here are a few possible takeaway points:

1. Big data is complex data. As we go out and collect more data from a finite world, we’re necessarily going to start collecting more and more interdependent data. Back when we had hundreds of people in our databases, it was plausible that none of our data examples were socially connected. But when our databases are significant fractions of the world population, we are much farther away from the controlled samples of good laboratory science. This means…
2. Data science as it’s currently practiced is essentially bad science. When we take a biased, dependent population of samples and try to generalize a conclusion from it, we need to be fully aware of how flawed our study is. That doesn’t mean things we discover using data analytics aren’t useful, but they need to be understood through the lens of the bias and complex dependencies present in the training data.
3. Computational methods should be aware of, and take advantage of, known dependencies. Some subfields of data mining and machine learning address this, like structured output learning, graph mining, relational learning, and more. But there is a lot of research progress needed. The data we’re mostly interested in nowadays comes from complex phenomena, which means we have to pay for accurate modeling with a little computational and cognitive complexity. How we manage that is a big open problem.

# Inner dual methods for structured output learning

One of the big challenges in making structured predictors more practical is that they can be really slow compared to the hack of assuming your variables are independent unstructured models.

There’s a line of research that partially addresses this expensiveness by avoiding repeated inference during the learning phase. I call it “inner-dual learning,” but it goes by many names.

The basic idea is that we do prediction by solving an optimization problem

$\arg\max_x f(x; \theta)$.

For example, the objective $f$ could be an energy and an entropy, which would make this optimization related to variational marginal inference in probabilistic models, or it could just be a linear objective over a structured output space, which is typical in combinatorial structured prediction. For various reasons, we often solve these inference objectives using a dual version of the inference optimization

$\arg\min_\alpha g(\alpha; \theta)$,

where

$\min_\alpha g(\alpha; \theta) = \max_x f(x; \theta)~\text{and}~g(\alpha; \theta) \ge f(x; \theta), \forall x, \alpha$

.

The learning optimization often takes the form of

$\min_\theta ~ R(\theta) + \max_x f(x; \theta) + \text{something}$

which is a saddle-point problem minimizing over parameters $\theta$ and maximizing over the predictions $x$. The “something” is typically a function of $\theta$ that doesn’t depend on $x$.

The standard way to solve saddle-point-y things like this is to repeatedly

1. solve the inner inference optimization,
2. take the (sub)gradient with respect to the parameters $\theta$, and

Having to solve the inference for each gradient step is painful, especially when you’re dealing with complex structured outputs. So the inner-dual idea is to replace that inner maximization with a minimization of its dual. (For real duals of concave functions, this forms an upper bound on the original learning objective!)

$\min_{\theta, \alpha} R(\theta) + g(\alpha; \theta) + \text{something}$.

The problem then becomes a joint minimization over the parameters and the dual variables! Moreover, we often have very fast message-passing style algorithms for solving the dual minimization. That means we can, in a principled way, interleave learning and inference, rather than using one as a subroutine for the other. The learning loop then becomes

1. make a single-pass update to the inner inference dual variables (e.g., pass messages),
2. take the (sub)gradient of the dual objective with respect to the parameters $\theta$, and

As far as I know, the first such inner-dual method was done in the seminal paper by Ben Taskar and folks at ICML ’05 (link). That paper is really well cited and has been read by tons of people, but seemingly few have picked up on this trick. Instead, I usually see it cited for the primal structured-output learning objective they introduced, which has been the foundation of a lot of related work. Part of the reason for the lack of recognition for this idea is that Ben et al. formulated the dual as a quadratic program that had to be passed into a general-purpose quadratic programming tool, which I imagine is super slow.

Years later in 2010, Ofer Meshi and folks (link), and Tamir Hazan and Raquel Urtasun (link) used the same idea but using the dual objectives from fast message-passing algorithms for graphical model inference as the inner dual. Later on in 2012, Alex Schwing and folks (link) used this for latent variable modeling, also using message-passing duals. In 2015, in work with Stephen Bach, Jordan Boyd-Graber, and Lise Getoor, we used the inner dual method twice to even more aggressively dualize expensive inferences during latent variable learning (link). We did this specifically for hinge-loss MRFs and with ADMM inference, but I’m working with my current students on extending this to be more general now. Also last year in 2015, Chen, Schwing et al. revisited the inner dual idea to train deep models with structured predictors attached to them (link).

I’m sure there are other examples of this trick in the literature, though one problem with finding it is that it hasn’t been consistently named. Both the Taskar and Hazan (et al.) papers don’t really give it a name, referring to the idea as just a dual objective; Meshi et al. refer to the idea as using a dual loss; Bach and I referred to it as inner dual (or in our case, since there were two dual inferences for latent variable learning, we called it paired dual learning); and Chen/Schwing et al. called it blending inference and learning. My preference is inner dual, as should be obvious by how I refer to it throughout this post. I think it captures the fact that we’re using the dual objective of the inner optimization. But pay attention for these other names of it!

While inner-dual methods seem to do a great job of alleviating the computational cost of learning, they still train models that are expected to run expensive inference at test time. That’s not great. There are related lines of research on training structured predictors that will do something cheap at test time, like truncate a message passing optimization, but it remains to be seen how to integrate these different approaches without nullifying their benefits.

# Scientific Hypothesis: We are the Best

It’s reviewing season for the summer conferences, so here’s something that’s on my mind as I’m doing my reviews.

One crappy thing that happens a lot in machine learning research is that researchers do non-scientific things like over-claiming, taking ownership, and bad experiment design. We end up with paper after paper, each claiming to present the best method with cherry-picked experiments that only demonstrate that the authors can draw prettier curves than other authors.

Sometimes authors use phrases like “our method” a lot in their description of the approach they’re demonstrating. Sometimes I even see tables or plots describing the final results from experiments where the legend entries are “our method,” “So and so’s method,” “SVM,” etc. This type of naming hints at a lack of objectivity.

Naming the proposed method is usually better, especially when the name actually describes the thing (so not an acronym that uses a letter from the middle of one of the words… c’mon people). Then the authors become scientists trying to understand the properties of some approach they discovered. And yes, they still get credit for discovering it, they just get fewer eye rolls.

This attitude also encourages poor experiment design. As computer scientists, we should want to understand the behavior of certain algorithms, so really good experiments would test many hypotheses about how the new algorithm performs under different conditions. We want to understand the strengths, weaknesses, and tradeoffs in comparison to other known methods. But many experiments in papers only test one hypothesis: “our method is the best method ever and you should purchase it.”

This problem is bad enough that I almost never trust the results of experiments in papers, or I always just think of them as synthetic sanity checks, even when they are using real data.

I’m certainly also quite guilty of this unscientific attitude and behavior. It’s very hard to avoid. On one hand, as scientists, we want to advance the world’s knowledge on machine learning, but on the other hand, as people who do science for a living, we want credit for advancing the world’s knowledge. That often leads to our papers reading more like patent applications than descriptions of scientific discovery. Yuck.

In conclusion, I’ve pointed out an annoyance and proposed no great solution for it. So I guess this qualifies as just ranting. But my method of pointing out this problem improves upon the state-of-the-art method by so-and-so et al. by 11%.

# On Rejection and Acceptance Rates

A while ago, I posted about the emotionally difficult challenges of research. I mentioned half-jokingly at the end of that post that I would in the future write a post about another challenge: rejection.

Since some of the students in my group just submitted their first papers to the peer review process, I figured I’d actually go through with that plan now. We just submitted three papers to the KDD research track, which, when I last checked, has an acceptance rate of just under 20%. That means a few things. In expectation, 0.6 of my group’s papers will be accepted, and the MAP estimate (and marginal decoding) of how many papers will be accepted is zero.

Of course, the actual likelihood of acceptance or rejection is dependent on the quality of the work, but as we’ve seen recently from, e.g., the NIPS experiment, paper quality doesn’t have as certain an effect as we’d hope. What makes a scientific contribution worthy of acceptance is a very subjective concept, so even the best papers have a chance of landing some reviewers who just won’t be convinced.

So given these realizations, when submitting work for peer review, one must be somewhat prepared for rejection. It sounds easy, right? We know acceptance rates are low; we know it’s not personal; we know the reviewers that decide our fates are doing the best they can with very limited time. If we were perfectly rational, logic-based beings, there’d be no problem here. Just keep improving your work and trying again and again.

Of course, we aren’t purely rational and logical. Being rejected is one of the most difficult and painful parts of a researcher’s life. It genuinely hurts. As scientists, we want to be rational about it, but the visceral reaction to reading “we regret to inform you” comes with a plethora of painful emotions, from disappointment and sadness, to fear and anger.

The reason I thought it might be useful to write a post like this is similar to that of my previous post inspired by the TED talk. Scientists are often trained to ignore these emotions. We don’t talk about them much. We often try to only discuss the rational, actionable parts of rejection. “Use the feedback, and make the research better.” But the reality for me is closer to “get feedback, feel terrible, doubt yourself, blame system, blame yourself, briefly consider quitting, feel embarrassed for having these reactions, seek support from non-scientist friends and family, get back to work pretending you’re not hurt, eventually really get back to work.”

This whole ordeal is invariably part of the job. But like the emotional challenge of facing uncertainty and “the cloud” in research, it would be helpful to acknowledge that it is okay, normal, and expected to have these emotional reactions. That doesn’t preclude the more rational advice I’ve seen around, but I’d like not to perpetuate the fantasy that we can be perfectly rational about this whole process.

Eventually, once we realize that these emotions are normal, perhaps then it will be easier to filter them. Then we can find which emotions are useful, and work toward getting the ones that are not useful (i.e., most of them) out of our systems. Perhaps knowing that these emotions are a shared experience can help us manage them more easily.

# Upcoming AISTATS paper

In about a week, our paper Unifying Local Consistency and MAX SAT Relaxations for Scalable Inference with Rounding Guarantees by Steve, me, and Lise will appear at AISTATS in San Diego. (Steve will be giving a talk on it Monday morning.)

The paper title is a mouthful, and it includes a pretty technical result, so here’s a weak attempt at explaining the intuition and take-away messages.

The paper is about MAP inference, or finding the most likely state in a probability distribution. Specifically, it’s about MAP inference in what we are calling logical Markov random fields (MRFs), which are MRFs whose potentials are defined by weighted logical clauses of a particular form. We show equivalences between two different approaches (and a third bonus one) for approximating MAP inference in these logical MRFs. These equivalences are theoretically interesting, but at least as importantly, they allow us to get the benefits of each approach, leading to fast MAP approximations that have constant-factor approximation guarantees.

What’s special about logical MRFs is that MAP inference is equivalent to finding the maximum weighted satisfying assignment to the logical variables, aka the MAX SAT problem. On the surface, this equivalence doesn’t seem exciting, because it equates one NP-hard problem to another. What makes it exciting is that there are some nice approximation algorithms for MAX SAT with quality guarantees, and these algorithms can therefore be applied to get quality guarantees for MAP. Unfortunately, the approximation method by the famous computer science duo, Michael Goemans and David Williamson, requires solving a linear program (LP) that scales not-so-well in practice, when using off-the-shelf linear programming algorithms.

Another approach for approximating MAP inference borrows from recent developments on doing fast inference in MRFs using local-consistency relaxations. At a very high level, these approaches relax the space of possible marginal probabilities (i.e., the marginal polytope) to a simpler space that only requires local consistency between marginal probabilities of variables and factors (i.e., the local marginal polytope). By solving the corresponding optimization over this simpler, relaxed set of constraints, many very fast message-passing algorithms have been discovered in the past few years. So it’s natural to try to use one of these local-consistency relaxation message-passing algorithms to do MAP inference in a logical MRF.

The main result we show in the paper is that these two seemingly different approaches are equivalent. This equivalence means that when we use these fast-in-practice local-consistency relaxation algorithms that pass messages to quickly find an approximate solution, we’re also able to get the solution to the linear-program subproblem of the MAX SAT approximation algorithm. Using the LP solution, we can perform a special rounding scheme that guarantees a constant-factor approximation.

The last bonus equivalence is that both of these approaches are also equivalent to the linear form of a hinge-loss Markov random field, which we’ve been studying over the past few years as a powerful class of probabilistic models with efficiently optimizable energy functions. The conversion from logic to hinge-loss MRFs (i.e., the principles behind probabilistic soft logic) had previously been motivated by connections to fuzzy logic, and now we have these other relationships to MAX SAT relaxation and local-consistency relaxation.

Behind the scenes, this last bonus piece is how we happened to find these equivalences. We initially were working with these hinge-loss MRFs and we had thought that these other approaches to doing inference in logically-defined MRFs seemed so different, that it’d be interesting to compare them. So we ran a few tests and discovered they were behaving similarly… very similarly; they were returning solutions with differences that were small enough to be numerical errors. This surprising behavior led to confusion, derivations, and finally understanding.

Finally, the super weird part: any (nondeterministic factored) discrete MRF can be converted to an equivalent logical MRF. This, in some sense, means the constant-factor quality guarantees that come from the equivalence between logical MRF inference and MAX SAT, also apply to any discrete MRF. But along the way of converting a discrete MRF to the restricted logical MRF form, the strength of this constant-factor guarantee must be weakened, especially since we know that MAP can’t be approximated to a constant factor unless P = NP. But it’s still an open question how this all fits together. Check out the paper, and maybe we can brainstorm about this in San Diego.

# Our NIPS 2014 Workshop papers

Two of our papers appeared at the NIPS 2014 workshops this past week.

• On the Collective Stability of Variational Inference,” by Ben London, me, and Lise Getoor, shows some of our theoretical analyses on bounding the curvature of variational entropy surrogates. Since a lot of inference methods get around the computational difficulty of computing and optimizing the entropy of graphical models, people often replace the entropy term with a convex surrogate that’s efficient to work with. In the paper, we specifically analyze two of these: tree reweighting, and region-based counting-number adjustment. We provide new, tighter bounds on how strongly convex tree entropies can be, and provide new conditions for the counting numbers of regions that guarantee strongly convex entropies (whereas the previous conditions only guaranteed strict convexity). In both cases, we identify conditions under which the modulus of strong convexity does not grow as the number of variables grows, which our previous theory suggests is necessary for generalization.
• Rounding Guarantees for Message-Passing MAP Inference with Logical Dependencies,” by Stephen H. Bach, me, and Lise Getoor, recounts our recent discovery that the local LP relaxation that is extremely popular for fast inference in discrete MRFs is actually equivalent to an old LP-based approximation algorithm for weighted MAX SAT, for a certain class of graphical models. This equivalence implies that the local LP relaxations, which our community has developed some blazing-fast algorithms to solve, automatically inherits the 3/4 approximation guarantees associated with the old MAX SAT method. And even better, the equivalence class also happens to include a huge subset of hinge-loss MRFs, which we’ve been looking at over the past few years.

Thanks to everyone who came to talk to us during the workshops! I was bouncing back and forth between the two workshops during the poster times, but the conversations I had were super interesting and helpful.

# Data Science Research for Social Good

In a few weeks, there will be a workshop at KDD on data science for social good, run by Rayid Ghani and folks. Rayid has also been heading the Data Science for Social Good fellowship program the past couple years.

I really love the whole mission behind the workshop and fellowship (and Stephen H. Bach, Lise Getoor, and I have submitted a short paper to the workshop on how probabilistic soft logic is particularly useful for problems that have social benefit). But I wanted to point out a distinction that I think will help bring in more of the best minds in machine learning research to applications with potential to do social good.

My view of the mission behind the existing effort to encourage social good applications of data science is that it is driven by the question, “What can state-of-the-art data science do to benefit society?”

This is an unarguably important question, and answers to this question should improve the lives of many immediately. The projects that are being tackled by the Data Science for Social Good Fellows should have measurable impact on the well-being of people now, in 2014. This type of immediate impact is crucially missing from most research, making it rather attractive to spend research effort on these problems.

On the other hand, what can easily be lost in the excitement over immediate tangible impact is the advancement of scientific knowledge, in algorithms or theory. When working on applied machine learning research, one typically explores what known, existing methods can be applied to novel problems.

Because of this tendency, I suggest emphasizing another important question, which exists in all novel applications to some degree, but is often paid less attention. The question is, “What can’t state-of-the-art data science do to benefit society?” I.e., what are we missing, that we need new algorithms, new models, or new theory to support?

We have developed a huge toolbox of machine learning over the past few decades, so the first question is a completely valid one to focus solely on, but it happens so often that the form of data relevant to new problems is intrinsically different from the assumed form of known tools. This discrepancy means that we often need new machine learning research to do data analysis, whether that is truly new, undiscovered research, or simply new research that has only recently been discovered.

For example, human data is inherently social and thus contains statistical dependencies that make it an ill-fit for traditional statistical tools that rely on independent samples. While machine learning research has developed methods to handle heavily dependent and structured data over the past decade, these methods are often overlooked in practice. The technology transfer has not been fully or successfully executed between researchers and practitioners.

Part of the reason for all the excitement over data science is that everyone is noticing the gap created as knowledge of machine learning and analytic tools is outpacing their application in the real world. Most of the energy now is in filling that gap by finding new applications, and this direction is completely justified. We have not filled this gap yet as a whole, but as we start using machine learning on new applications, we will start inverting parts of this gap by identifying situations where known machine learning tools are insufficient for the problems we want to solve. These situations are where a lot of important scientific research can happen, and I can think of few better settings where I want this to happen than the context of social good.

# Research in “the cloud” and the honeymoon phase

A few days ago, I watched a TED talk by physicist Uri Alon on the emotional experience of scientific research. It is a fun talk, and I thought the message is important.

See the video here.

Uri argues that science is presented in a manner that poorly sets up expectations for scientists: the presented story is that we scientists brilliantly devise a hypothesis, run some experiments, and verify this hypothesis. Then we hit print and science is done. Instead, Uri sheds light on the actual process, which involves a taxing trek through what he calls “the cloud.” The real story is that a scientist has a hypothesis, tests it, finds that it is wrong, and then enters this cloud, which is a place of uncertainty, despair, and confusion. The scientist has to challenge his or her basic assumptions, and only by doing so, will be able to produce a new hypothesis that truly advances human knowledge.

Though Uri is a physicist, I think this message is just as relevant for computer science. I can’t speak for all fields within computer science, but at least in machine learning research, this is almost always the way progress occurs.

One problem of applying Uri’s message to computer science is the nomenclature. The cloud (or is it the Cloud?) is a buzzword that is already somewhat defined (but not very well). So using it in this context could lead to confusion (which is a bit too meta to be useful). We need another term for the computer science version of the cloud. Or we could just use it and stop using “the cloud” to describe the Internet, because we already have a word for that.

I would add to the process Uri describes another important concept to prepare researchers for the emotional roller coaster of science: the honeymoon phase.

The honeymoon phase is what I call the period when I’ve come up with an idea, perhaps it’s an algorithm, a theorem, or an application, that I think will work. As I start incrementally testing the idea–coding up the algorithm, for example–it starts to seem more and more correct. A subroutine of the algorithm works exactly as it should on paper! The learning algorithm correctly learns from a synthetic data set! If we assume a lemma, the proof actually works out! These small victories invoke a sense of euphoria and often come with daydreams of how easily this new research will lead to publication and recognition.

In reality, the honeymoon phase is almost always followed by a discovery that something is wrong, which leads to a sharp turn directly into the cloud. This contrast from the highs of the honeymoon phase to the lows of the cloud is jarring.

Like the message from the TED talk, I believe acknowledging that this sharp transition is part of a shared experience could help limit the emotional distress cause by the process of research. I’m not sure if there is any particular strategy for intelligently handling the highs of the honeymoon phase better, and I’m hesitant to suggest to anyone not to enjoy it while it’s happening.

Next time on Terrible Emotions in Science: Rejection…


text:
# Confused about arrays in C [closed]

Hey guys I am learning the basics of C language and I am a little bit confused about how to use arrays.

I mean what are they used for?

## closed as off-topic by Alexandre Vaillancourt♦, Josh♦Jan 15 '16 at 16:19

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "Programming questions that aren't specific to game development are off-topic here, but can be asked on Stack Overflow. A good rule of thumb is to ask yourself "would a professional game developer give me a better/different/more specific answer to this question than other programmers?"" – Alexandre Vaillancourt, Josh
If this question can be reworded to fit the rules in the help center, please edit the question.

• This should be on stackoverflow since this is not related to gamedev. – DH. Jan 15 '16 at 16:09
• I would recommend to you first learn how to use the language (C or C++… your choice) before attempting to develop a game, on your first question you asked about a basic 2D game, but if you don't know how to use the language, then that will be almost impossible to do at the moment – rlam12 Jan 15 '16 at 16:21
• Sorry...I was too excited about developing. – Jithesh Jan 16 '16 at 5:57

That's an array of type std::string[]. Or if you want to get really technical, it could be considered an array of type ItemConsumable[] (because "Steve" is a valid string, but you certainly can't buy him!)

In game programming, you would just arrays (or lists) to keep track of objects, actions, events, or other data. It entirely depends on the use. You might even have a (two dimensional!) array that your units use for pathfinding.

• String must be std::string. – HolyBlackCat Jan 15 '16 at 16:10
• @HolyBlackCat You would be correct. I don't work in C so my syntax and proper declarations are more than rusty, but examples are valid no matter what language. – Draco18s Jan 15 '16 at 16:12
• That's ok, answer and examples are good. I just decided to tell it to you instead of editing. – HolyBlackCat Jan 15 '16 at 16:14
• @HolyBlackCat Just edit it, dude, I won't be offended. :) I've accepted a couple of edits where the editor was more correct than I had been (variable naming, for instance), or for minor things like syntax errors or spelling. Comments just makes me think, "FFS, just edit it yourself." – Draco18s Jan 15 '16 at 16:17

First of all. C is not the same as C++. (They are different programming languages)

Now, (trying to explain without making it too complicated), arrays are lists of variables.

(The image has Numbers with capital letters, my fail, ignore that, shouldn´t have the starting letter in capitals)

For example, int numbers[10]; is an array that contains space for 10 ints (numbers).

You can access values from the array ("list"):

exampleIntVariable = numbers[1];

Our variable will have the value of the 2ND number in our list (The first one is numbers[0])

format: plain


text:
# What tools do you use most?

### Help Support HomeBuiltAirplanes.com:

#### wally

##### Well-Known Member
I was sitting on a plastic milk crate today working on my cowl parts and was thinking about what tools I might have that would make the job easier. I couldn't think of any. I wanted to trim and fit slowly so I didn't go too far and have to make another of what I was making.

That got me thinking about what tools I or anyone really needed to build an airplane.

So this is a short list of what tools I use most.

A small 2ft by 2ft stand with a 4" vise and 6" grinder on it. I can move it close to where I am working.

A couple of hammers, including a plastic face one.

Hack saw.

Files: a 12" mill file for straightening snipped sheet metal edges and lots of other shaping jobs, a couple of rat-tail files and a chain-saw blade sharpening file. The chain-saw file is nice for small inside curves. It is smooth cut and they come in a couple of sizes.

LH aircraft snips, (red handle) and rh?? green handle offset snips. I could not get along without my offset snips.

I use an X-acto knife w/#11 blade a lot for trimming stuff and even for enlarging or "adjusting" holes in aluminum.

3/8 electric drill and a bunch of bits and a couple of 100 degree countersinks and a rotary file cutter.

oxy-acetylene torch set from Harbor Freight. The bottles cost over twice as much as the torch but I can weld 4230 tubing, yea! Building my engine mount myself saved enough to pay for it.

Small air compressor.

A $20.00 spray gun also from Harbor Freight.$6.00 muffler hammer that I use as a rivet gun!!! Hey, it works. I was surprised that the .401 dia rivet sets fit it just fine. If I was building a Vans RV-something, I would for sure get a real 2X rivet gun tho.

some screwdrivers and wrenches.

I am lucky that where I work we have a bench roll to curve the sheets for my cowl and very luck our EAA chapter has a 10ft bending brake for the rare times I need to make long bends.

Scrap wood for backup when drilling parts and for clamping aluminum between to make shorter bends in metal.

Poster board, masking tape, and scissors for making paper patterns that I then trace on aluminum.

And that is about it. Sure there a LOT of other tools I could have but so far I have been doing just fine with this.

So don't think you need a 30x30 hangar and a Snap-On truck full of tools and equipment to build an airplane. Start little and add just what you need to do a job.

#### cgwendling

##### Well-Known Member
To build my basic airframe I have used very few tools.
Table saw
power mitre saw, hand mitre saw
block plane
sharp chisels
sand paper, sanders
router
drill, bits
clamps, over 100
plastic spoons and cups (to mix epoxy)
stapler

These are the ones that I use in just about every stage of the airframe. There will be a few rivits, bolts, cloth, wiring, fuel system and misc that I will use other tools on but not very much.

#### Rhino

##### Well-Known Member
Originally posted by wally
What tools do you use most?
My brain ...... I hope!

#### Craig

##### Well-Known Member
Best Tool

The best tool I can think of would be a replacement for your milk crate.

That thing will give you waffle butt, and limit your thinking time.

Get a comfortable shop chair, one that you can sit in and ponder your next move, or how to complete the one that you just started. A small cooler to hold some tea or lemonade also helps.

Having said that, I think one of my most-used tools are my measuring tools - 25' tape, 18" steel ruler - flexible - and little 6" steel ruler. And a good fine-point Sharpie pen that marks on just about anything (NOTE: Do NOT use on fabric!!! - that is what pencils are for!).

#### Sonnyj

##### Well-Known Member
new nose gaer

Hi All
Well building or rebuilding ( in my case ) a single seat gyro copter is in my humble opinion is much less daunting than any fixed wing I can think of whitch makes me very envious of you folks who have undertakin such projects. Most guys just go out and buy gyro parts and bolt them on and go flyin in their flying lawnchair. But I am a little more hands on than that. I use my drill\mill, metal lath and upright band saw the most, along with the micrometers and rules and hand tools.I also have a milk crate but have ducktaped a cusion to it "I hate waffle butt".
It's just relaxing to setup and make somthing out in the shop and getaway from the hassles of the day job.
Happy hamerin guys
Sonny

#### Attachments

• 66.3 KB Views: 563

#### Sonnyj

##### Well-Known Member
Almost done

I have more to do but this is what I have sofar.
Cheers
Sonny

#### Attachments

• 83.4 KB Views: 619

#### ZENO

##### Well-Known Member

I have an old Sears jig saw that was made out of stamped sheet metal. It uses these little 3 inch blades and makes as thin a kerf as I've ever seen. I wouldn't part with it or replace it for anything. The up/down jig movement is very little which makes it so accurate.

It's my secret weapon for rib parts. The Baby Lakes has 28 ribs and most of them have 57 parts each. I'm doing my 3rd set of wings now.

Also, I can do just about anything with my table saw.

#### ZENO

##### Well-Known Member

I have an old Sears jig saw that was made out of stamped sheet metal. It uses these little 3 inch blades and makes as thin a kerf as I've ever seen. I wouldn't part with it or replace it for anything. The up/down jig movement is very little which makes it so accurate.

It's my secret weapon for rib parts. The Baby Lakes has 28 ribs and most of them have 57 parts each. I'm doing my 3rd set of wings now.

Also, I can do just about anything with my table saw.

#### ZENO

##### Well-Known Member
The disc on my belt disc sander is great for forming aluminum parts. I use a scrap of 1/16 ply for the aluminum to rest on so the shavings and table/rest don't scratch the piece. I use a small drum sander on my drill press for inside curves. What a beautiful and accurate job it does.

I also have one of those small roll around stools with a shelf on it.

I've built cars and motorcycles and in comparison you need almost no tools at all to build airplanes. What a great hobby.

ZENO :ban:

#### Greg Mueller

##### Well-Known Member
CNC mill

(couldn't resist)

#### gahan

##### Well-Known Member
Iv'e accumulated many tools since my youth but every thing I've needed to build my max yould fit in 2 shoe boxes, a few things I've found in yard sales have proven very usefull , Old table saw with table extension, NO SAW JUST TABLE, easy to clamp to farily large.
small drill press that excepts your hand drill also dremmell attachment found both at yard sales over past 3 years About \$5, the Jig saw mentioned above is truley the most productive tool you can have, place upside down in vise clamp lightly,Real lightly,turn bottom plate around for small slot to front wala.
Small Riobie belt and disk sander to finisn to length and match angles 3 or 4 drill bits if you don't drop the drill you'll never need to replacement bit.

#### Attachments

• 41.8 KB Views: 203


text:
Home Robust Loess : Java library
 I am attempting to create a regression model that best describes my data. Due to it's nature, I'd like to fit a quadratic polynomial, using robust loeass regression. In matlab, I'd run the following command to achieve this, where 0.1 is the bandwidth: smooth(x,y,0.1,'rloess')  The closest thing I've found to this in Java land is the apache math3 library, as shown in this post . I can use this library as follows: final LoessInterpolator rloess = new LoessInterpolator(0.1, LoessInterpolator.DEFAULT_ROBUSTNESS_ITERS) rloess.smooth(xval, yval);  However, LoessInterpolator seems to only perform linear regression, which I do not desire. Is it possible to "enable" the quadratic model in the apache math3 library?


text:
# Finding a “lowest” path in a graph

I have an undirected graph $G = (E,V)$, $|V|=n$, where each node $v_i$ has a natural number weight. Think of these weights as heights $h_i$. Given two nodes $s$ and $t$, I'd like to find a lowest simple path between $s$ and $t$, a path whose average height is minimal among all simple paths. If $\rho = (s{=}v_1, v_2, \ldots, v_{k-1}, v_k{=}t)$ is a path, its average height is $(h_1 + \cdots + h_k)/k$. The path $\rho$ must be simple, i.e., no vertex repeated.

I am not seeing an efficient algorithm. If it helps, assume $G$ is planar.

• This problem is btw (somewhat) related to the min-average cost cycle in directed graphs, which can be solved in polynomial time. – Sariel Har-Peled Jul 12 '18 at 20:12

Consider an instance $(V',E')$ of directed Hamilton path that asks for a Hamilton path from vertex $x\in V'$ to vertex $y\in V'$. We create the following instance of the lowest path problem in an undirected graph $G=(V,E)$ from it:
• Every vertex $v\in V'$ is replaced by three new vertices $v_1,v_2,v_3$, together with the two edges $\{v_1,v_2\}$ and $\{v_2,v_3\}$.
• For every arc $(v,u)\in E'$, we introduce the undirected edge $\{v_3,u_1\}$ in graph $G$.
• All edges $\{v_2,v_3\}$ in $G$ with $v\ne x$ and $v\ne y$ have weight 1, and all the remaining edges have weight 0.
• The starting point of the desired lowest path is vertex $x_2$, and the endpoint is vertex $y_2$.
Consider a path $P$ in $G$ from $x_2$ to $y_2$, and let $k$ denote the number of weight $1$ edges on $P$.Then $P$ must also contain (at least) $3k+4$ edges of weight $0$, so that the average weight is at most $k/(4k+4)$. This expression is at most $|V'|/(4|V'|+4)$. A Hamilton cycle in $G'$ translates into a path with average weight $|V'|/(4|V'|+4)$ in $G$.


text:
# Research

### Overall Objectives

The VeriDis project team includes members of the MOSEL group at LORIA, the computer science laboratory in Nancy, and members of the research group Automation of Logic at Max-Planck-Institut für Informatik in Saarbrücken. It is headed by Stephan Merz and Christoph Weidenbach. VeriDis was created in 2010 as a local research group of Inria Nancy – Grand Est and has been an Inria project team since July 2012.

The objectives of VeriDis are to contribute to advances in verification techniques, including automated and interactive theorem proving, and to make them available for the formal development and analysis of concurrent and distributed algorithms and systems, within the framework of mathematically precise and practically applicable development methods. We intend to assist designers of algorithms and systems in carrying out formally proved developments, where proofs of relevant properties, as well as bugs, can be found with a high degree of automation.

Verification techniques based on theorem proving are already having substantial impact. In particular, they have been successfully applied to the verification and analysis of sequential programs, often in combination with static analysis and software model checking. Ideally, systems and their properties would be specified in high-level, expressive languages, errors in specifications would be discovered automatically, and finally, full verification could also be performed completely automatically. Due to the inherent complexity of the problem, this cannot be achieved in general. We have, however, observed significant advances in theorem proving in recent years. We are particularly interested in the integration of different deduction techniques and tools, such as automated theorem proving for relevant theories, such as different fragments of arithmetic. These advances suggest that a substantially higher degree of automation can be achieved in system verification than what is available in today’s verification tools.

VeriDis aims at exploiting and further developing automation in system verification, and at applying its techniques within the context of concurrent and distributed algorithms, which are by now ubiquitous and whose verification is a big challenge. Concurrency problems are central for the development and verification of programs for multi- and many-core architectures, and distributed computation underlies the paradigms of grid and cloud computing. The potential of distributed systems for increased resilience to component failures makes them attractive in many contexts, but also makes formal verification important and challenging. We aim at moving current research in this area to a new level of productivity and quality. To give a concrete example: today the designer of a new distributed protocol may validate it using testing or model checking. Model checking will help finding bugs, but can only guarantee properties of a high-level model of the protocol, usually restricted to finite instances. Testing distributed systems and protocols is notoriously difficult because corner cases are hard to establish and reproduce. Also, many testing techniques require an executable, whose production is expensive and time-consuming, and since an implementation is needed, errors are found only when they are expensive to fix. The techniques that we develop aim at automatically proving significant properties of the protocol already during the design phase. Our methods mainly target designs and algorithms at high levels of abstraction; we aim at components of operating systems, distributed services, and down to the (mobile) network systems industry.

## Results

#### IsaFoL: Isabelle Formalization of Logic

Joint work with Andreas Halkjær From (DTU Copenhagen), Alexander Birch Jensen (DTU Copenhagen), Maximilian Kirchmeier (TU München), Peter Lammich (TU München), John Bruntse Larsen (DTU Copenhagen), Julius Michaelis (TU München), Tobias Nipkow (TU München), Nicolas Peltier (IMAG Grenoble) Anders Schlichtkrull (DTU Copenhagen), Dmitriy Traytel (ETH Zürich), and Jørgen Villadsen (DTU Copenhagen).

Researchers in automated reasoning spend a significant portion of their work time specifying logical calculi and proving metatheorems about them. These proofs are typically carried out with pen and paper, which is error-prone and can be tedious. As proof assistants are becoming easier to use, it makes sense to employ them.

In this spirit, we started an effort, called IsaFoL (Isabelle Formalization of Logic), that aims at developing libraries and methodology for formalizing modern research in the field, using the Isabelle/HOL proof assistant.https://bitbucket.org/isafol/isafol/wiki/Home Our initial emphasis is on established results about propositional and first-order logic. In particular, we are formalizing large parts of Weidenbach’s forthcoming textbook, tentatively called Automated Reasoning—The Art of Generic Problem Solving.

The objective of formalization work is not to eliminate paper proofs, but to complement them with rich formal companions. Formalizations help catch mistakes, whether superficial or deep, in specifications and theorems; they make it easy to experiment with changes or variants of concepts; and they help clarify concepts left vague on paper.

The repository contains 14 completed entries and four entries that are still in development. Notably, Mathias Fleury formalized a SAT solver framework with learn, forget, restart, and incrementality. This year he extended it with key optimizations such as the two-watched-literal procedure. The corresponding paper, written together with Jasmin Blanchette and Peter Lammich, was accepted at a highly competitive conference (CPP 2018).

#### Extension of Term Orders to $\lambda$ -Free Higher-Order Logic

Superposition is one of the most successful proof calculi for first-order logic today, but in contrast to resolution, tableaux, and connections, it has not yet been generalized to higher-order logic (also called simple type theory). Yet, most proof assistants and many specification languages are based on some variant of higher-order logic.

This motivates us to design a graceful generalization of superposition: a proof calculus that behaves like standard superposition on first-order problems and that smoothly scales up to arbitrary higher-order problems. A challenge is that superposition relies on a simplification order, which is fixed in advance of the proof attempt, to prune the search space.

We started our investigations by focusing on a fragment devoid of $\lambda$ -abstractions, but with partial application and application of variables, two crucial higher-order features. We generalized the two main orders that are used in superposition-based provers today—the lexicographic path order (LPO) [article] and the Knuth-Bendix order (KBO) [article]. The new orders gracefully generalize their first-order counterparts and enjoy nearly all properties needed for superpositions. An exception is compatibility with contexts, which is missing for LPO and some KBO variants. Preliminary work suggests that we can define a version of the superposition calculus that works well in theory and practice (i.e., is refutationally complete and does not lead to a search-space explosion) despite the missing property.

#### A Fine-Grained Approach of Understanding First-Order Logic Complexity

By the introduction of the separated fragment [article] we have initiated a new framework for a fine-grained understanding of the complexity of fragments of first-order logic, with and without the addition of theories. We have related the classes of the polynomial hierarchy to subclasses of the separated fragment [article] and developed new decidability results [article], [article] based on the techniques of our framework for the combination of the Bernays-Schoenfinkel subfragment with linear arithmetic.

#### Theorem Proving Based on Approximation-Refinement into the Monadic Shallow Linear Fragment with Straight Dismatching Constraints

We have introduced an approximation-refinement approach for first-order theorem proving based on counterexample-guided abstraction refinement [article]. A given first-order clause set is transformed into an over-approximation contained in the fragment of monadic, shallow, linear clauses with straight dismatching constraints. We have shown the fragment to be decidable, strictly extending known results. If the abstraction obtained that way is satisfiable, so is the original clause set. However, if it is unsatisfiable, then the approximation provides a terminology for lifting the found refutation, step by step, into a proof for the original clause set. If lifting fails, the cause is analyzed to refine the original clause set such that the found refutation is ruled out for the future, and the procedure repeats. We have shown that this approach is superior to all known calculi on certain classes of first-order clauses. In particular, it is able to detect satisfiability of clause sets that have only infinite models.

#### Combination of Satisfiability Procedures

Joint work with Christophe Ringeissen from the PESTO project-team of Inria Nancy – Grand Est, and Paula Chocron at IIIA-CSIC, Bellaterra, Catalonia, Spain.

A satisfiability problem is often expressed in a combination of theories, and a natural approach consists in solving the problem by combining the satisfiability procedures available for the component theories. This is the purpose of the combination method introduced by Nelson and Oppen. However, in its initial presentation, the Nelson-Oppen combination method requires the theories to be signature-disjoint and stably infinite (to ensure the existence of an infinite model). The design of a generic combination method for non-disjoint unions of theories is difficult, but it is worth exploring simple non-disjoint combinations that appear frequently in verification. An example is the case of shared sets, where sets are represented by unary predicates. Another example is the case of bridging functions between data structures and a target theory (e.g., a fragment of arithmetic).

In 2015, we defined [article] a sound and complete combination procedure à la Nelson-Oppen for the theory of absolutely free data structures (including lists and trees) connected to another theory via bridging functions. This combination procedure has also been refined for standard interpretations. The resulting theory has a nice politeness property, enabling combinations with arbitrary decidable theories of elements. We also investigated other theories [article] amenable to similar combinations: this class includes the theory of equality, the theory of absolutely free data structures, and all the theories in between.

In 2017, we have been improving the framework and unified both results. A new paper is in preparation.

#### Quantifier Handling in SMT

Joint work with Andrew J. Reynolds, Univ. of Iowa, USA.

SMT solvers generally rely on various instantiation techniques for handling quantifiers. We built a unifying framework encompassing quantified formulas with equality and uninterpreted functions, such that the major instantiation techniques in SMT solving can be cast in that framework. It is based on the problem of E-ground (dis)unification, a variation of the classic Rigid E-unification problem. We introduced a sound and complete calculus to solve this problem in practice: Congruence Closure with Free Variables (CCFV). Experimental evaluations of implementations of CCFV demonstrate notable improvements in the state-of-the-art solver CVC4 and make the solver veriT competitive with state-of-the-art solvers for several benchmark libraries, in particular those originating in verification problems. This was the subject of a publication [article]. In later, unpublished work, we are revisiting enumerative instantiation for SMT. This effort takes place in the context of the Matryoshka project.

#### Non-Linear Arithmetic in SMT

In the context of the SMArT ANR-DFG (Satisfiability Modulo Arithmetic Theories), KANASA and SC ${}^{2}$ projects (cf. sections 59 and 82), we study the theory, design techniques, and implement software to push forward the non-linear arithmetic (NLA) reasoning capabilities in SMT. This year, we designed a framework to combine interval constraint propagation with other decision procedures for NLA, with promising results, notably in the international competition of SMT solvers SMT-COMP 2017. We also studied integration of these procedures into combinations of theories. The ideas are validated within the veriT solver, together with code from the raSAT solver (from JAIST). An article is in preparation.

We also adapted the subtropical method to use in an SMT context, with valuable results. This was the subject of a publication in 2017 [article].

#### Proofs for SMT

We have developed a framework for processing formulas in automatic theorem provers, with generation of detailed proofs. The main components are a generic contextual recursion algorithm and an extensible set of inference rules. Clausification, skolemization, theory-specific simplifications, and expansion of `let’ expressions are instances of this framework. With suitable data structures, proof generation adds only a linear-time overhead, and proofs can be checked in linear time. We implemented the approach in the SMT solver veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced, which is important for independent checking and reconstruction in proof assistants. This was the subject of a publication in  [article]. This effort takes place in the context of the Matryoshka project.

#### Coding Modal and Description Logics in SAT solvers

The application scenario behind this research is the verification of graph transformations, which themselves are relevant for a wide range of practical problems such as pointer structures in imperative programs, graph databases or access control mechanisms.

Graph structures can typically be perceived as models of modal logics, and modal logics and variants (such as description logics that are the basis for the web ontology language OWL) are in principle suitable specification formalisms for graph transformations. It turns out, however, that pure modal logics are often not sufficiently expressive for the intended verification purpose and that extensions are needed for which traditional proof methods such as tableau calculi become complex: the termination of the calculi are often very difficult to prove, and huge efforts are required to obtain an efficient implementation.

For these reasons, we have explored methods of encoding the above-mentioned logics in SAT and SMT solvers such as CVC4 and veriT. The idea is to traverse the formula to be verified in order to span up a pre-model that possibly contains more elements (worlds in a Kripke structure) than the real model, and then to run a solver to find out which of these elements can effectively be realized. A prototype has been implemented, with encouraging results. It remains to connect this prototype to the graph verification engine and to publish this work.

#### Work on the TLA+ Proof System

We continued our work on encoding set-theoretic formulas in multi-sorted first-order logic, and in particular for SMT solvers. Specifically, we unified and streamlined a technique combining an injection of unsorted expressions into sorted languages, simplification by rewriting, and abstraction that underlies the SMT backend of the TLA+ proof system TLAPS. A presentation of our technique was accepted in the journal Science of Computer Programming, to appear in 2018.

The proof of the join protocol in a pure-join variant of the Pastry protocol [article] implementing a distributed hash table over a peer-to-peer network is the largest case study carried out so far within TLAPS. Consisting of roughly 30k lines of proof, it was developed as part of Noran Azmy’s PhD thesis, defended at the end of 2016 [article]. A presentation of the design of the protocol and its proof was accepted in the journal Science of Computer Programming, to appear in 2018.

#### Automated Analysis of Systems of ODE for Multistationarity

Joint work with R. Bradford and J. Davenport (Bath, UK), M. England (Coventry, UK), H. Errami, C. Hoyt, and A. Weber (Bonn, Germany), V. Gerdt (Dubna, Russia), D. Grigoriev (Lille, France), O. Radulescu (Montpellier, France)

We considered the problem of determining multiple steady states for positive real values in models of biological networks. Investigating the potential for these in models of the mitogen-activated protein kinases (MAPK) network has consumed considerable effort using special insights into the structure of corresponding models. We have applied combinations of symbolic computation methods for mixed equality/inequality systems, specifically automated deduction methods like virtual substitution, lazy real triangularization and cylindrical algebraic decomposition. We have determined multistationarity of an 11-dimensional MAPK network when numeric values are known for all but potentially one parameter. More precisely, our considered model has 11 equations in 11 variables and 19 parameters, 3 of which are of interest for symbolic treatment, and furthermore positivity conditions on all variables and parameters [article].

Subsequent work [article] demonstrates that our techniques benefit tremendously from a new graph theoretical symbolic preprocessing method. We apply our combined techniques to visualize of parameter regions for multistationarity. Comparing computation times and quality of results it turns out that our automated deduction-based approach clearly outperforms established numerical continuation methods.

While automated deduction technology is a bit under the hood here, this interdisciplinary research line addresses important questions related to contemporary research in systems biology. With researchers from that area very actively involved, the results are recognized also within their communities.

#### Making Explicit Domain Knowledge in Formal System Development

Joint work with partners of the IMPEX project.

As explained in the description of the IMPEX project in section 59, we advocate that formal modeling languages should explicitly represent the knowledge resulting from an analysis of the application domain, and that ontologies are good candidates for handling explicit domain knowledge. Our objective in doing so is to offer rigorous mechanisms for handling domain knowledge in design models.

We developed the notion of dependency for state-based models. Context-awareness is an important feature in system design. We argue that in proof systems and conceptual modelling this notion should be highlighted precisely. Since we focus on conceptual modelling, understandability and clarity are of high importance. We introduce a new definition [article] for proof context in state-based formalisms with an application to the Event-B modeling language. Furthermore, we introduce a dependency relation between two Event-B models. The contextualization of Event-B models is based on knowledge provided from domains that we classified into constraints, hypotheses and dependencies. The dependency mechanism between two models makes it possible to structure the development of systems models, by organizing phases identified in the analyzed process. These ideas are inspired by work based on the modelling of situations in situation theory that emphasize capabilities of type theory with regard to situation modelling to represent knowledge. Our approach is illustrated on small case studies, and was validated on a development of design patterns for voting protocols.

#### Incremental Development of Systems and Algorithms

Joint work with Manamiary Bruno Andriamiarina, Neeraj Kumar Singh (IRIT, Toulouse), Rosemary Monahan (NUI Maynooth, Ireland), Zheng Cheng (LINA, Nantes), and Mohammed Mosbah (LaBRI, Bordeaux).

The development of distributed algorithms and, more generally, of distributed systems, is a complex, delicate, and challenging process. The approach based on refinement applies a design methodology that starts from the most abstract model and leads, in an incremental way, to a distributed solution. The use of a proof assistant gives a formal guarantee on the conformance of each refinement with the model preceding it.

Our main result during 2017 is the development of a proved-based pattern for integrating the local computation models and the Visidia platform [article].

#### Modeling Network Flows in View of Building Security Chains

We are working on the application of formal modeling and verification techniques in the area of network communications, and in particular for constructing security functions in a setting of software-defined networks (SDN). Concretely, Nicolas Schnepf defined an extension of the Pyretic language [article] taking into account both the control and the data planes of SDN controllers and implemented a translation of that extension to the input languages of the nuXmv model checker and of SMT solvers. This work was published at NetSoft 2017 [article].

Extending this approach, we have worked on inferring probabilistic finite-state automata models that represent network flows generated by Android applications. The objective is to exploit this representation for generating security chains that detect significant deviations from the behavior represented by the automata and can initiate protective actions. Comparing our models with automata produced by the state-of-the-art tools Invarimint and Synoptic, we obtain representations that are as succinct as those inferred by Invarimint, and significantly smaller than Synoptic, but that include information about transition probability, which Invarimint does not. This work was accepted for publication at NOMS 2018.

#### Satisfiability Techniques for Reliability Assessment

Joint work with Nicolae Brînzei at Centre de Recherche en Automatique de Nancy.

The reliability of complex systems is typically assessed using probabilistic methods, based on the probabilities of failures of individual components, relying on graphical representations such as fault trees or reliability block diagrams. Mathematically, the dependency of the overall system on the working status of its components is described by its Boolean-valued structure function, and binary decision diagrams (BDDs) have been used to construct a succinct representation of that function. We explore the use of modern satisfiability techniques as an alternative to BDD-based algorithms. In [article], we develop three different algorithms for computing minimal tie sets (i.e., component configurations that ensure that the system is functioning). Our algorithms are based on either conjunctive or disjunctive normal form representations of the structure function or on the Hasse diagram representing the configurations. These algorithms have been prototypically implemented in Python, and we are evaluating them on existing benchmarks in order to understand which algorithm works best for typical fault dependencies.

#### Statistical evaluation of the robustness of production schedules

Joint work with Alexis Aubry, Sara Himmiche, Pascale Marangé, and Jean-François Pétin at Centre de Recherche en Automatique de Nancy.

Finding a good schedule for a production system, especially when it is flexible and when several machines can perform the same operation on products, is a challenging and interesting problem. For a long time, operations research has provided state-of-the-art methods for optimizing scheduling problems. However, approaches based on Discrete Event Systems present interesting alternatives, especially when dealing with uncertainties on the demand or the production time. In this particular case, the flexibility of the automata-based modeling approach is really useful. Using probabilistic timed automata, we demonstrated [article] that statistical model checking can be used successfully for evaluating the robustness of a given schedule w.r.t. probabilistic variations of the processing time. We were thus able to compare different schedules based on their level of service (i.e., the probability that the system will complete the production process within a deadline slightly higher that the schedule time) and their sensitivity (the minimal deadline for which the level of service is greater than a given threshold) [article].

An interdisciplinary workshop on this topic was organized jointly with our colleagues of Centre de Recherche en Automatique and funded by Fédération Charles Hermite.

#### Using Cubicle for Verifying TLA+ Specifications

Cubicle http://cubicle.lri.fr is a model checker for the verification of parameterized transition systems whose state is described by arrays of variables indexed by an abstract sort representing processes. During her internship, Poonam Kumari designed a translation algorithm from a restricted class of TLA+ specifications into the input language of Cubicle. A prototypical implementation demonstrates the feasibility of the approach, although more work will be necessary to widen the scope of the translation. This work will be continued within the PARDI project, described in section 59.


text:
### Learning objectives

• Be able to describe the different data types R uses
• Use c(), str(), class(), and typeof() to make and investigate vectors
• Understand coercion between data types
• Know how factors work under the hood
• Be able to manipulate factors

# Why Learn This Stuff?

It can be helpful to think of R, and your computer in general, as a collaborator who speaks a different language from you and is remarkably pedantic, but remarkably skilled as well. Learning a new language is difficult, and learning to speak it to an extremely literal and pedantic collaborator can make it even more frustrating. In such a collaboration, it might be useful to spend a little time learning the fundamentals of the language, understanding how you might interpret things differently, and not just rushing to “data data data!”

While this stuff might not be the most exciting material, or even feel useful right now, it is remarkably important in laying the groundwork for a fruitful collaboration with R. Skipping past this stuff and rushing to the finish line can leave you with a) error messages that don’t make sense to you, b) problems that are difficult to Google solutions to, and c) problems that R never even warns you about, because R didn’t think there was anything wrong!

All that being said, building a solid understanding of these fundamental ideas will save you headaches in the future, and leave you more well equipped to deal with new projects and concepts.

## Vectors and data types

Vectors are the most basic way that R deals with data. A vector is made up of a series of values, which could be numbers or characters. Remember when we learned how to assign values to objects, like x <- 5? Once we do that, x is a vector with a length of 1. Basically everything in R will be a vector or a bunch of vectors bound together in some way, so knowing how vectors work is crucial to working with more complex data structures.

We can bind together a series of values into a vector using the c() function. For example we can create a vector of animal weights and assign it to a new object weight_g:

weight_g <- c(50, 60, 65, 82)
weight_g
## [1] 50 60 65 82

A vector can also contain characters:

animals <- c("mouse", "rat", "dog")
animals
## [1] "mouse" "rat"   "dog"

The quotes around “mouse”, “rat”, etc. are essential here. Without the quotes R will assume there are objects called mouse, rat and dog. As these objects don’t exist in R’s memory, there will be an error message. You can use either single ' or double " quotes for characters.

There are many functions that allow you to inspect the content of a vector. length() tells you how many elements are in a particular vector:

length(weight_g)
## [1] 4
length(animals)
## [1] 3

An important feature of a vector is that all of the elements are the same type of data. The function class() indicates the class (the type of element) of an object:

class(weight_g)
## [1] "numeric"
class(animals)
## [1] "character"

The function str() provides an overview of the structure of an object and its elements. It is a useful function when working with large and complex objects.

str(weight_g)
##  num [1:4] 50 60 65 82
str(animals)
##  chr [1:3] "mouse" "rat" "dog"

A vector can be modified, adding values to the start or end of it. You can use the c() function to add other elements to your vector:

weight_g <- c(weight_g, 90) # add to the end of the vector
weight_g <- c(30, weight_g) # add to the beginning of the vector
weight_g
## [1] 30 50 60 65 82 90

In the first line, we take the original vector weight_g, add the value 90 to the end of it, and save the result back into weight_g. Then we add the value 30 to the beginning, again saving the result back into weight_g.

An atomic vector is the simplest R data structure and is a linear vector of a single type. Above, we saw 2 of the main atomic vector types that R uses: "character" and "numeric" (or "double"), which are numbers that can include decimals. These are the basic building blocks that all R objects are built from. There are 2 other atomic vector types that you’ll often encounter:

• "logical" for TRUE and FALSE (the boolean data type)
• "integer" for integer numbers (e.g., 2L, the L indicates to R that it’s an integer)

There are some other types, like complex and raw but you’ll rarely, if ever, encounter them, so we won’t go into them further.

You can check the type of your vector using the typeof() function and inputting your vector as the argument. typeof() is similar to class(), but it digs even deeper down to the bare bones of how R thinks about data. The difference is less important now, but we’ll come back around to it.

### Challenge

• We’ve seen that atomic vectors can be of type character, numeric (or double), integer, and logical. But what happens if we try to mix these types in a single vector?

• What will happen in each of these examples? (hint: use class() to check the data type of your objects):

num_char <- c(1, 2, 3, "a")
num_logical <- c(1, 2, 3, TRUE)
char_logical <- c("a", "b", "c", TRUE)
tricky <- c(1, 2, 3, "4")
• Why do you think it happens?

• How many values in combined_logical are "TRUE" (as a character) in the following example:

num_logical <- c(1, 2, 3, TRUE)
char_logical <- c("a", "b", "c", TRUE)
combined_logical <- c(num_logical, char_logical)
• You’ve probably noticed that objects of different types get converted into a single, shared type within a vector. In R, we call converting objects from one class into another class coercion. These conversions happen according to a hierarchy, whereby some types get preferentially coerced into other types. Can you draw a diagram that represents the hierarchy of how these data types are coerced?

## Subsetting vectors

If we want to extract one or several values from a vector, we must provide one or several indices in square brackets.

animals <- c("mouse", "rat", "dog", "cat")
animals[2] # could be read as "return the second value in animals"
## [1] "rat"
animals[c(3, 2)] # could be read as "return the third and second values in animals"
## [1] "dog" "rat"

We can also repeat the indices to create an object with more elements than the original one:

animals[c(1, 2, 3, 2, 1, 4)]
## [1] "mouse" "rat"   "dog"   "rat"   "mouse" "cat"

R indices start at 1. Programming languages like Fortran, MATLAB, Julia, and R start counting at 1, because that’s what human beings typically do. Languages in the C family (including C++, Java, Perl, and Python) count from 0 because that’s simpler for computers to do.

### Conditional subsetting

Another common way of subsetting is by using a logical vector. TRUE will select the element with the same index, while FALSE will not:

weight_g <- c(21, 34, 39, 54, 55)
weight_g[c(TRUE, FALSE, TRUE, TRUE, FALSE)] # could be read as "give me the first value, not the second value, etc."
## [1] 21 39 54

Typically, these logical vectors are not typed by hand, but are the output of other functions or logical tests. For instance, if you wanted to select only the values above 50:

weight_g > 50    # will return logicals with TRUE for the indices that meet the condition
## [1] FALSE FALSE FALSE  TRUE  TRUE
## so we can use this to select only the values above 50
weight_g[weight_g > 50]
## [1] 54 55

You can combine multiple tests using & (both conditions are true, AND) or | (at least one of the conditions is true, OR):

weight_g[weight_g < 30 | weight_g > 50]
## [1] 21 54 55
weight_g[weight_g >= 30 & weight_g == 21]
## numeric(0)

Here, < stands for “less than”, > for “greater than”, >= for “greater than or equal to”, and == for “equal to”. The double equal sign == is a test for numerical equality between the left and right hand sides, and should not be confused with the single = sign, which performs variable assignment (similar to <-).

A common task is to search for certain strings in a vector. One could use the “or” operator | to test for equality to multiple values, but this can quickly become tedious. The function %in% allows you to test if any of the elements of a search vector are found:

animals <- c("mouse", "rat", "dog", "cat")
animals[animals == "cat" | animals == "rat"] # returns both rat and cat
## [1] "rat" "cat"
animals %in% c("rat", "cat", "dog", "duck", "goat")
## [1] FALSE  TRUE  TRUE  TRUE
animals[animals %in% c("rat", "cat", "dog", "duck", "goat")]
## [1] "rat" "dog" "cat"

### Challenge

• Can you figure out why "four" > "five" returns TRUE?

### Vector Math and Recycling

You can do basic mathematical operations with vectors in R. We won’t get into this too deeply, but you should be aware of how R approaches these operations.

You can add a number to a vector of numbers like this:

x <- 1:10

x + 3
##  [1]  4  5  6  7  8  9 10 11 12 13

Or multiply all the values in a vector by a number:

x * 10
##  [1]  10  20  30  40  50  60  70  80  90 100

By default, R will do value-by-value math. So if you add together two vectors of equal length, R will return a vector of the 1st value of each added together, then the 2nd value of each added together, etc. Let’s take a look here:

y <- 100:109

x + y
##  [1] 101 103 105 107 109 111 113 115 117 119

As you can see, the first entry we get back is 1 + 100, the second is 2 + 101, and so on. What happens if we try to add two vectors that aren’t the same length?

z <- 1:2

x + z
##  [1]  2  4  4  6  6  8  8 10 10 12

Whoa… what happened here? R does something called recycling. It adds together the first values of each vector, then the second values, but then it runs out of values in vector z. It then recycles the values of z, so it will add the 3rd value of x to the 1st value of z, then the 4th value of x to the 2nd value of z, and so on. Essentially, it recycles z from 1,2 into 1,2,1,2,1,2,1,2,1,2, then does the addition.

We actually already saw this behavior: when we added 3 to x, 3 gets recycled into a vector of 3s that is the same length as x.

Since the length of x is 10, it is a multiple of the length of z, which is 2. What happens if the longer vector isn’t a multiple of the shorter one?

z <- 1:3

x + z
## Warning in x + z: longer object length is not a multiple of shorter object length
##  [1]  2  4  6  5  7  9  8 10 12 11
a <- x + z
## Warning in x + z: longer object length is not a multiple of shorter object length

R warns us about this! However, if you try to assign this result to an object, we get the warning, but the assignment works. z will get recycled until it reaches the length of x. So z gets recycled from being 1,2,3 to being 1,2,3,1,2,3,1,2,3,1, then gets added to x. This can give you unexpected results if you’re doing math with vectors and you’re not paying attention to what’s going on.

Recycling also happens with logical vectors:

x[c(TRUE, FALSE)]
## [1] 1 3 5 7 9
x[c(TRUE, FALSE, FALSE)]
## [1]  1  4  7 10

As mentioned earlier, logical vectors are often generated as intermediate steps when we’re subsetting. If you’re not careful about the lengths of these intermediate logical vectors, you can get some funky results without even noticing how they happened.

## Missing data

As R was designed to analyze datasets, it includes the concept of missing data (which is uncommon in other programming languages). Missing data are represented in vectors as NA.

When doing operations on numbers, most functions will return NA if the data you are working with include missing values. This feature makes it harder to overlook the cases where you are dealing with missing data. You can add the argument na.rm=TRUE to calculate the result while ignoring the missing values.

heights <- c(2, 4, 4, NA, 6)
mean(heights)
## [1] NA
max(heights)
## [1] NA
mean(heights, na.rm = TRUE)
## [1] 4
max(heights, na.rm = TRUE)
## [1] 6

If your data include missing values, you may want to become familiar with the functions is.na(), na.omit(), and complete.cases(). See below for examples.

## Extract those elements which are not missing values.

is.na(heights) # this returns a logical vector with TRUE where there is an NA
## [1] FALSE FALSE FALSE  TRUE FALSE
!is.na(heights) # the ! means "is not", so now we get a logical vector with FALSE for NAs
## [1]  TRUE  TRUE  TRUE FALSE  TRUE
heights[!is.na(heights)] # now we put that logical vector in, and it will NOT return the entries with NA
## [1] 2 4 4 6
## Extract those elements which are complete cases. The returned object is an atomic vector of type "numeric" (or "double").
heights[complete.cases(heights)]
## [1] 2 4 4 6

Recall that you can use the typeof() function to find the type of your atomic vector.

### Challenge

1. Using this vector of heights in inches, create a new vector with the NAs removed.
heights <- c(63, 69, 60, 65, NA, 68, 61, 70, 61, 59, 64, 69, 63, 63, NA, 72, 65, 64, 70, 63, 65)
1. Use the function median() to calculate the median of the heights vector.
2. Use R to figure out how many people in the set are taller than 67 inches.

# Other Data Structures

Vectors are one of the many data structures that R uses. Other important ones are lists (list), data frames (data.frame), matrices (matrix), arrays (array), and factors (factor). These are all built from combinations of vectors, so much of what you learned about vectors will be important when working with these data structures.

## Lists

Lists are the most fundamental way that R works with multiple vectors. A list is simply a bunch of vectors put together. The vectors can be different data types, so a list could hold a character vector with the names of your sampling sites as well as a numeric vector with their percent tree cover.

Lists are extremely flexible, and you’ll come across them a lot in various shapes and sizes. We’ll talk about them a bit more in later lessons.

## Data Frames

Data frames are the most common way we work with tabular data in R. Data frames at their core are just picky lists. A data frame is a list where every vector has to be the same length, which is akin to every column having the same number of rows. This means a data frame is rectangular, which is why it matches up with tabular data we’re used to working with. A list could have one vector that has 5 values and one vector that has a thousand.

## Matrices and Arrays

Matrices (2D) and Arrays (3D or more) are similar to dataframes and lists, but they are a little more barebones. Matrices and arrays must be made of a single type of data, no mixing types across different columns like in a dataframe. We won’t work with these much, but you might encounter them if you do something like population modeling in R. If you remember your basics of vectors, you should be pretty well equipped to tackle matrices and arrays.

## Factors

Factors are a bit funky, and they can be equally useful and frustrating. Factors look a lot like 1-dimensional character vectors, but they behave a bit differently.

Factors are used to represent categorical data. Let’s make one to play around with:

sex <- factor(c("male", "female", "female", "male"))
class(sex)
## [1] "factor"

If we ask for the class of sex, we see that it’s a factor. Let’s try using typeof(), which goes a little deeper:

typeof(sex)
## [1] "integer"

An integer???

Factors are really just integer vectors with character labels attached to them.

Once created, factors can only contain a pre-defined set of values, known as levels. By default, R always sorts levels in alphabetical order. For instance, in our sex factor, R will assign the integer 1 to the level "female" and 2 to the level "male" (becausef comes before m, even though the first value in sex is "male"). You can see this by using the function levels() and you can find thenumber of levels using nlevels():

levels(sex)
## [1] "female" "male"
nlevels(sex)
## [1] 2

Sometimes, the order of the factors does not matter, other times you might want to specify the order because it is meaningful (e.g., “low”, “medium”, “high”), it improves your visualization, or it is required by a particular type of analysis. Here, one way to reorder our levels in the sex vector would be:

sex # current order
## [1] male   female female male
## Levels: female male
sex <- factor(sex, levels = c("male", "female"))
sex # after re-ordering
## [1] male   female female male
## Levels: male female

In R’s memory, these factors are represented by integers (1, 2, 3), but are more informative than integers because factors are self describing: "female", "male" is more descriptive than 1, 2. Which one is “male”? You wouldn’t be able to tell just from the integer data. Factors, on the other hand, have this information built in. It is particularly helpful when there are many levels (like the species names in our example dataset).

### Converting factors

If you need to convert a factor to a character vector, you use as.character(x).

as.character(sex)
## [1] "male"   "female" "female" "male"

Converting factors where the levels appear as numbers (such as concentration levels, or years) to a numeric vector is a little trickier. The as.numeric() function returns the index values of the factor, not its levels, so it will result in an entirely new (and unwanted in this case) set of numbers. One method to avoid this is to convert factors to characters, and then to numbers.

year_fct <- factor(c(1990, 1983, 1977, 1998, 1990))
as.numeric(year_fct)               # Wrong! And there is no warning...
## [1] 3 2 1 4 3
as.numeric(as.character(year_fct)) # This does the trick
## [1] 1990 1983 1977 1998 1990

### Renaming factors

You can rename the levels using the levels() function

levels(sex)
## [1] "male"   "female"
levels(sex)[1]
## [1] "male"
levels(sex)[1] <- "MALE"
sex
## [1] MALE   female female MALE
## Levels: MALE female
levels(sex) <- c("MALE", "FEMALE")
sex
## [1] MALE   FEMALE FEMALE MALE
## Levels: MALE FEMALE

### Challenge

• Copy, paste and run the code below in your R script:
treatment <- factor(c("high", "low", "low", "medium", "high"))
• First, re-order the levels of treatment so that “low” is first, “medium” is second, and “high” is third. Hint: Use the factor() function again, but with an additional levels argument.
• Next, check the names with the levels() function, then use this same function to rename the levels of treatment to “L”, “M” and “H”
treatment <- factor(c("high", "low", "low", "medium", "high"))
treatment <- factor(treatment, levels = c("low", "mediam", "high"))
levels(treatment) <- c("L", "M", "H")
treatment
## [1] H    L    L    <NA> H
## Levels: L M H

### Why Factors?

Factors can be convenient at times, and they will pop up pretty frequently, but in most circumstances, character strings will give you fewer hassles. It’s usually best to start with character vectors, and convert them explicitly to factors if you need to.

Some functions in R will automatically convert character strings to factors. For instance, read.csv() run in older versions R will turn any character data into factors, while in newer versions this has been changed to keep them as characters. If you aren’t sure, you can use the argument stringsAsFactors=FALSE in read.csv() to make sure your character strings as character strings.

This lesson is adapted from Data Carpentry’s Ecology Workshop Introduction to R


text:
Review question

Can we find an integer solution to three simultaneous inequalities? Add to your resource collection Remove from your resource collection Add notes to this resource View your notes for this resource

Ref: R5281

Solution

From the inequalities $y-2x>0,\qquad x+y>3,\qquad 2y-x<5$ deduce that $\frac{1}{3}< x < \frac{5}{3},\qquad 2< y <\frac{10}{3}$

Consider the three inequalities in the plane:

• $y-2x = 0$ crosses the axes at $(0,0)$ and has gradient $2$ (it rearranges to $y=2x$). The region $y-2x>0$ lies above this line, as it includes the point $(0,1)$.

• $x+y =3$ crosses the axes at $(0,3)$ and $(3,0)$. The region $x+y>3$ lies above this line, as it does not include the point $(0,0)$.

• $2y-x =5$ crosses the axes at $(0,\frac52)$ and $(-5,0)$. The region $2y-x<5$ lies below this line, as it includes the point $(0,0)$.

We can therefore sketch these three regions in the plane. Here the shaded regions are those which do not satisfy the inequality.

We can see from our sketch that there is a small triangular region satisfied by all three inequalities. We determine where each pair of lines intersects in order to determine the coordinates of the vertices of this triangle. \begin{align*} y=2x\quad&\text{and}\quad x+y=3 \quad &\Longrightarrow \quad&& x&=1,& y&=2 \\ y=2x\quad&\text{and}\quad 2y-x=5 \quad &\Longrightarrow \quad&& x&=\tfrac53,& y&=\tfrac{10}{3} \\ x+y=3\quad&\text{and}\quad 2y-x=5 \quad &\Longrightarrow \quad&& x&=\tfrac13,& y&=\tfrac{8}{3} \end{align*}

From these we can deduce the minumum and maximum extent of both $x$ and $y$: $\frac{1}{3} < x < \frac{5}{3}, \qquad 2< y < \frac{10}{3},$ as required.

… and hence that the given inequalities cannot be satisfied simultaneously by integral values of $x$ and $y$.

The only integer value of $x$ that satisfies $\frac{1}{3} < x < \frac{5}{3}$ is $x=1$.

The only integer value of $y$ that satisfies $2< y < \frac{10}{3}$ is $y=3$.

Does the point $(1,3)$ obey all three inequalities simultaneously? \begin{align*} y-2x &> 0: \quad 3-2=1>0 \quad \checkmark \\ x+y &>3: \quad 1+3=4>3 \quad \checkmark \\ 2y-x &<5: \quad 6-1=5 \nless 5 \quad \mathsf{X} \end{align*}

Thus there is no integer pair of $x$ and $y$ that satisfies all three inequalities simultaneously.


text:
# Proving $\sum_{k=1}^m{k^n}$ is divisible by $\sum_{k=1}^m{k}$ for $n=2013$

I got an interesting new question, it's about number theory and algebra precalculus. Here is the question:

a positive integer $n$ is called valid if $1^n+2^n+3^n+\dots+m^n$ is divisible by $1+2+3+\dots+m$ for every positive integer $m$.

1. Prove that 2013 is valid
2. Prove that there are infinite positive integers which are not valid

Every little hint, contribution and recommendation would be very helpful. Sorry for my bad english. Thanks before.

• Hint: $1^{2013}+n^{2013}$ is divisible by $n+1$. So is $2^{2013}+(n-1)^{2013}$ – Thomas Andrews Jun 3 '13 at 13:09
• Hint: tell us where you got the question. Then, tell us why it interests you. Then tell us what you have been able to do with it, and where you get stuck. – Gerry Myerson Jun 3 '13 at 13:16
• There aren't any infinite positive integers. You mean infinitely many different positive integers (each one finite). – Marc van Leeuwen Jun 3 '13 at 13:21

## 3 Answers

If $n$ is odd, then modulo $m+1$ we have $2(1^n + 2^n + \ldots + m^n) = (1^n+m^n) + (2^n+(m-1)^n) + \ldots + (m^n+1^n) \\ \equiv (1^n-1^n) + (2^n-2^n) + \ldots + (m^n-m^n) = 0 \pmod {m+1}$.

Also, since $m^n \equiv 0 \pmod m$, $2(1^n + 2^n + \ldots + m^n) \equiv 2(1^n + 2^n + \ldots + (m-1)^n) \equiv 0 \pmod m$

Since $m$ and $m+1$ are coprime, this shows that $2(1^n + \ldots + m^n)$ is a multiple of $m(m+1)$, and since $m(m+1)$ is even, $1^n + \ldots + m^n$ is a multiple of $m(m+1)/2 = 1+2+\ldots+m$.

If $n$ is even then $1+2^n \equiv 2 \pmod 3$, which is not a multiple of $1+2 = 3$

All odd $n$ are valid. In fact, for all odd $n$, $1^n + 2^n + 3^n + \dots + m^n$ is actually a polynomial in $1 + 2 + 3 + \dots + m = m(m+1)/2$. These polynomials are known as Faulhaber polynomials (see https://en.wikipedia.org/wiki/Faulhaber%27s_formula#Faulhaber_polynomials). You can find a proof of this fact in the AMM article "Sums of Powers of Integers" (modifying the proof slightly also shows the divisibility relation you want, but there are also easier ways to do this; see mercio's solution).

To answer your second question, all even $n$ are not valid; this can be easily seen by noticing that $2^n + 1$ is not divisible by $3$ if $n$ is even.

• Even knowing that the Faulhaber polynomials have zero coefficients in degree zero doesn't give you the result above, of course, since they have rational coefficients, so knowing about these polynomials still leaves something to argue. – Thomas Andrews Jun 3 '13 at 13:23
• Since the polynomials do not appear to have integer coefficients, it is not immediately clear to me why they would imply the divisibility condition. Could you explain that? – Marc van Leeuwen Jun 3 '13 at 13:24
• Good point; the fact that they are polynomials doesn't imply that they are divisble by 1 + 2 + 3 + ... + m (I guess I wasn't thinking when I posted this). Still, I think the same inductive proof can be used to show that this divisibility relation holds (but I admit the other proof is much nicer, if you only want the divisibility fact). – Jon Schneider Jun 3 '13 at 13:35

Use the binomial theorem to expand $\sum k^n$.

• Could you provide a bit more explanation of how to do that? It is not immediately apparent. – robjohn Jun 4 '13 at 13:31


text:
# KSEEB SSLC Class 10 Maths Solutions Chapter 15 Surface Areas and Volumes Ex 15.1

KSEEB SSLC Class 10 Maths Solutions Chapter 15 Surface Areas and Volumes Ex 15.1 are part of KSEEB SSLC Class 10 Maths Solutions. Here we have given Karnataka SSLC Class 10 Maths Solutions Chapter 15 Surface Areas and Volumes Exercise 15.1.

## Karnataka SSLC Class 10 Maths Solutions Chapter 15 Surface Areas and Volumes Exercise 15.1

(Unless stated otherwise, take π $$=\frac{22}{7}$$)

Question 1.
2 cubes each of volume 64cm3 are joined end to end. Find the surface area of the resulting cuboid.
Solution:
If measurement of each side of each cube be l cm, then

(l)3 $$=\sqrt[3]{64}$$
∴ l = 4 cm.
Length of cubes if both joined together,
Length, l = 4 + 4 = 8 cm.
height, h = 4 cm.
Surface area of the cuboid,
= 2lb + 2lh + 2bh
= 2(8 × 4) + 2(8 × 4) + 2(4 × 4)
= 2 × 32 + 2 × 32 + 2 × 16 = 64 + 64 + 32
= 160 sq.cm.

Question 2.
A vessel is in the form of a hollow hemisphere mounted by a hollow cylinder. The diameter of the hemisphere is 14 cm and the total height of the vessel is 13 cm. Find the inner surface area of the vessel.
Solution:
(i) Diameter of a hollo hemisphere = 14 cm.
∴ Radius of a hollow hemisphere, r
r = 7 cm.
Inner curved surface of a hemisphere = 2π2

= 14 × 22
= 308 sq. cm.
(ii) Radius of hollow cylinder, r = 7 cm.
Height, h = 13 – 7 = 6 cm.
∴ Inner Surface area of the Cylinder,
= 2πrh
$$=2 \times \frac{22}{7} \times 7 \times 6$$
= 44 × 6
= 264 sq.cm.
∴ Inner surface area of the vessel = Area of hemisphere + Area of cylinder
= 308 + 264
= 572 sq. cm.

Question 3.
A toy is in the form of a cone of radius 3.5 cm mounted on a hemisphere of same radius. The total height of the toy is 15.5 cm. Find the total surface area of the toy.
Solution:
(i) Radius of base of circular toy,
r = 3.5 cm.
∴ Surface Area of hemisphere, = 2πr2

= 77 sq.cm
(ii) Let slant height of cone is l cm. then

∴ Curved surface area of a cone = πrl

= 137.5 sq.cm.
∴ Total surface area of a toy = Surface area of hemisphere + Curved surface area of a cone
= 77.0 + 137.5
= 214.5 sq.cm.

Question 4.
A cubical block of side 7 cm is surmounted by a hemisphere. What is the greatest diameter the hemisphere can have ? Find the surface area of the solid.
Solution:
(i) A cubical block of side 7 cm is surmounted by a hemisphere.
∴ Diameter of hemisphere is = 7 cm.
Radius of hemisphere, r = 3.5 cm.
∴ Surface area of hemisphere = Curved surface area – Area of base of hemisphere

= 38.5
(ii) The curved surface area of square,
=6 × l2
= 6 × (7)2
= 6 × 49
= 294 sq. cm.
∴ Total surface area of cubical block, = Curved surface area of cubical block + Surface area of hemisphere.
= 294 + 38.5
=332.5sq.cm.

Question 5.
A hemispherical depression is cut out from one face of a cubical wooden block such that the diameter l of the hemisphere is equal to the edge of the cube. Determine the surface area of the cube. Determine the surface area of the remaining solid.
Solution:
Let, Length of each edge of cubical block = Diameter of hemisphere = l
∴ Radius of hemisphere, $$r=\frac{l}{2} unit$$.

Total surface area of newly formed cube = Curved surface area of cube – Upper part of Cube + Area of hemisphere which is depressed

Question 6.
A medicine capsule is in the shape of a cylinder with two hemispheres stuck to each of its ends (see Figure given below). The length of the entire capsule is 14 mm and the diameter of the capsule is 5 mm. Find its surface area.

Solution:

(i) Surface area of cylindrical capsule, = 2πrh
$$=2 \pi \times\left(\frac{5}{2}\right) \times 9$$
= 45π mm2,
(ii) Surface area of both hemispheres,

= 25π mm2
∴ Total surface area of capsule, = 45π + 25π mm2
= 70π mm2
$$=70 \times \frac{22}{7}$$
= 220 mm2

Question 7.
A tent is in the shape of a cylinder surmounted by a conical top. If the height and diameter of the cylindrical part are 2.1m and 4m respectively, and the slant height of the top is 2.8 m, find the area of the canvas used for making the tent. Also, find the cost of the canvas of the tent at the rate of Rs. 500 per m2. (note that the base of the tent will not be covered with canvas.)
Solution:
(i) Radius of base of cylinder, r= 2 mm.
Height of base of cylinder, h= 2.1 m.
∴ Curved Surface area of cylinder = 2πrh
= 2π × 2 × (2.1)
$$=4 \times \frac{22}{7} \times 2.1$$
= 26.4 m2.

r = 2 m.
length, l = 2.8 m.
∴ Curved Surface area of cylinder = πrl
$$=\frac{22}{7} \times 2 \times 2.8$$
= 17.6 m2.
∴ Total area of the tent = 26.4 + 17.6
= 44m2
Cost of 1 aq.m. of canvas is Rs. 500.
Cost of 44 sq. m. canvas … ??
500 × 44
= Rs. 22,000.

Question 8.
From a solid cylinder whose height is 2.4 cm and diameter 1.4 cm, a conical cavity of the same height and same diameter is hollowed out. Find the total surface area of the remaining solid to the nearest cm2.
Solution:
Height of the cylinder, h = 2.4 m.
Diameter of the cylinder, d = 1.4 m.
∴ Radius, r = 0.7 m.
(i) Outer Curved surface area of cylinder = 2πrh

$$=2 \times \frac{22}{7} \times(0.7) \times 2.4$$
= 44. × 0.24
= 10.56 cm2.
(ii) Area of base of = πr2

= 1.54 cm2.
(iii) Inner surface area of cylinder, = πrl

= 5.5 cm2
∴ Total surface area of newly formed cube = 10.56 + 1.54 + 5.5 = 17.6 cm2.
∴ Nearest value is 18 sq.cm.

Question 9.
A wooden article was made by scooping out a hemisphere from each end of a solid cylinder, as shown in the figure. If the height of the cylinder is 10 cm. and its base is of radius 3.5 cm. find the total surface area of the article.

Solution:
Radius of base of cylinder, r= 3.5 cm
Height, h = 10 cm.

Total area of article, = Curved Surface area of Cylinder + 2 × Area of Hemisphere
= 2πrh + 2 × 2πr2

= 374 sq.cm.

We hope the given KSEEB SSLC Class 10 Maths Solutions Chapter 15 Surface Areas and Volumes Ex 15.1 will help you. If you have any query regarding Karnataka SSLC Class 10 Maths Solutions Chapter 15 Surface Areas and Volumes Exercise 15.1, drop a comment below and we will get back to you at the earliest.

error: Content is protected !!