An official website of the United States government
One approach to probabilistic inference involves counting the number of models of a given Boolean formula. Here, we are interested in inferences involving higher-order objects, i.e., functions. We study the following task: Given a Boolean specification between a set of inputs and outputs, count the number of functions of inputs such that the specification is met. Such functions are called Skolem functions.We are motivated by the recent development of scalable approaches to Boolean function synthesis. This stands in relation to our problem analogously to the relationship between Boolean satisfiability and the model counting problem. Yet, counting Skolem functions poses considerable new challenges. From the complexity-theoretic standpoint, counting Skolem functions is not only #P-hard; it is quite unlikely to have an FPRAS (Fully Polynomial Randomized Approximation Scheme) as the problem of synthesizing a Skolem function remains challenging, even given access to an NP oracle.The primary contribution of this work is the first algorithm, SkolemFC, that computes the number of Skolem functions. SkolemFC relies on technical connections between counting functions and propositional model counting: our algorithm makes a linear number of calls to an approximate model counter and computes an estimate of the number of Skolem functions with theoretical guarantees. Our prototype displays impressive scalability, handling benchmarks comparably to state-of-the-art Skolem function synthesis engines, even though counting all such functions ostensibly poses a greater challenge than synthesizing a single function.
more »
« less
Middle school students' development of an understanding of the concept of function using an applet with no algebraic representations
Abstract Middle school students (n = 144) worked with an applet specially designed to introduce the concept of function without using algebraic representations. The purpose of the study was to examine whether the applet would help students understand function as a relationship between a set of inputs and a set of outputs and to begin to develop a definition of function based on that relationship. Results indicate that, by focusing on consistency of the outputs, the students, at a rate of approximately 80%, are able to distinguish functions from nonfunctions. Also, students showed some promise in recognizing constant functions as functions, a known area of common misconceptions. Students' main conceptual difficulty, likely caused by the context, was accepting nonintuitive outputs even if those outputs were consistent.
more »
« less
- Award ID(s):
- 1820998
- PAR ID:
- 10559293
- Publisher / Repository:
- Wiley Online
- Date Published:
- Journal Name:
- School Science and Mathematics
- Volume:
- 123
- Issue:
- 6
- ISSN:
- 0036-6803
- Page Range / eLocation ID:
- 278 to 289
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Abstract Understanding microbial roles in ecosystem function requires integrating microscopic processes into food webs. The carnivorous pitcher plant,Sarracenia purpurea, offers a tractable study system where diverse food webs of macroinvertebrates and microbes facilitate digestion of captured insect prey, releasing nutrients supporting the food web and host plant. However, how interactions between these macroinvertebrate and microbial communities contribute to ecosystem functions remains unclear. We examined the role of the pitcher plant mosquito,Wyeomyia smithii, in top‐down control of the composition and function of pitcher plant microbial communities. Mosquito larval abundance was enriched or depleted across a natural population ofS. purpureapitchers over a 74‐day field experiment. Bacterial community composition and microbial community function were characterized by 16S rRNA amplicon sequencing and profiling of carbon substrate use, bulk metabolic rate, hydrolytic enzyme activity, and macronutrient pools. Bacterial communities changed from pitcher opening to maturation, but larvae exerted minor effects on high‐level taxonomic composition. Higher larval abundance was associated with lower diversity communities with distinct functions and elevated nitrogen availability. Treatment‐independent clustering also supported roles for larvae in curating pitcher microbial communities through shifts in community diversity and function. These results demonstrate top‐down control of microbial functions in an aquatic microecosystem.more » « less
-
Abstract Human impacts on ecosystems are resulting in unprecedented rates of biodiversity loss worldwide. The loss of species results in the loss of the multiple roles that each species plays or functions (i.e., “ecosystem multifunctionality”) that it provides. A more comprehensive understanding of the effects of species on ecosystem multifunctionality is necessary for assessing the ecological impacts of species loss. We studied the effects of two dominant intertidal species, a primary producer (the seaweedNeorhodomela oregona) and a consumer (the shellfishMytilus trossulus), on 12 ecosystem functions in a coastal ecosystem, both in undisturbed tide pools and following the removal of the dominant producer. We modified analytical methods used in biodiversity–multifunctionality studies to investigate the potential effects of individual dominant species on ecosystem function. The effects of the two dominant species from different trophic levels tended to differ in directionality (+/−) consistently (92% of the time) across the 12 individual functions considered. Using averaging and multiple threshold approaches, we found that the dominant consumer—but not the dominant producer—was associated with ecosystem multifunctionality. Additionally, the relationship between abundance and multifunctionality differed depending on whether the dominant producer was present, with a negative relationship between the dominant consumer and ecosystem function with the dominant producer present compared to a non‐significant, positive trend where the producer had been removed. Our findings suggest that interactions among dominant species can drive ecosystem function. The results of this study highlight the utility of methods previously used in biodiversity‐focused research for studying functional contributions of individual species, as well as the importance of species abundance and identity in driving ecosystem multifunctionality, in the context of species loss.more » « less
-
ABSTRACT Although the relationship between creativity andADHDis uncertain, recent studies examining how dimensionally assessed characteristics ofADHDrelate to creativity and divergent thinking in adults suggest an occasional positive, linear relationship between the constructs. However, the executive functions proposed to underlie characteristics ofADHDhave not been examined in relation to creativity. This study was conducted to determine how different characteristics ofADHDrelated to executive functioning (as assessed by the BrownADDScales) predict different components of figural divergent thinking, intellectual risk‐taking, and creative self‐efficacy. Undergraduate engineering students (N = 60) completed the BrownADDScales, a figural divergent thinking task, and self‐report measures of intellectual risk‐taking and creative self‐efficacy. A series of multivariate regression models demonstrated that several components of divergent thinking (i.e., fluency, originality, and resistance to closure) were predicted by different characteristics ofADHD. Although fluency was predicted by affect only and originality was predicted by activation only, resistance to closure was predicted by activation, effort, and attention. Additionally, intellectual risk‐taking was predicted by memory, effort, and activation, whereas creative self‐efficacy was predicted by effort. The implications of these results relating to the relationship betweenADHDand creativity, as well as for engineering undergraduate education are discussed.more » « less
-
Modular verification tools allow programmers to compositionally specify and prove function specifications. When using a modular verifier, proving a specification about a functionfrequires additional specifications for the functions called byf. With existing state of the art tools, programmers must manually write the specifications for callee functions. We present a counterexample guided algorithm to automatically infer these specifications. The algorithm is parameterized over a verifier, counterexample generator, and constraint guided synthesizer. We show that if each of these three components is sound and complete over a finite set of possible specifications, our algorithm is sound and complete as well. Additionally, we introducesize-boundedsynthesis functions, which extends our completeness result to an infinite set of possible specifications. In particular, we describe a size-bounded synthesis function for linear integer arithmetic constraints. We conclude with an evaluation demonstrating our technique on a variety of benchmarks. When using a modular verifier, proving a specification about a functionfrequires additional specifications for the functions called byf. With existing state of the art tools, programmers must manually write the specifications for callee functions. We present a counterexample guided algorithm to automatically infer these specifications. The algorithm is parameterized over a verifier, counterexample generator, and constraint guided synthesizer. We show that if each of these three components is sound and complete over a finite set of possible specifications, our algorithm is sound and complete as well. Additionally, we introducesize-boundedsynthesis functions, which extends our completeness result to an infinite set of possible specifications. In particular, we describe a size-bounded synthesis function for linear integer arithmetic constraints. We conclude with an evaluation demonstrating our technique on a variety of benchmarks.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript
- Journal Article:
- https://doi.org/10.1111/ssm.12622
