Hypernuclei

A baryon is a particle made of 3 quarks. The most familiar are the proton, which consists of two up quarks and a down quark, and the neutron, made of two downs and an up. Baryons containing strange quarks were discovered later, since the strange quark is more massive and soon decays to an up or down quark. A hyperon is a baryon that contains one or more strange quarks, but none of the still more massive quarks.

The first hyperon be found was the Λ, or lambda baryon. It’s made of an up quark, a down quark and a strange quark. You can think of it as a ‘heavy neutron’ in which one down quark was replaced by a strange quark. The strange quark has the same charge as the down, so like the neutron the Λ is neutral.

The Λ baryon was discovered in October 1950 by V. D. Hopper and S. Biswas of the University of Melbourne: these particles produced naturally when cosmic rays hit the upper atmosphere, and they were detected in photographic emulsions flown in a balloon. Imagine discovering a new elementary particle using a balloon! Those were the good old days.

The Λ has a mean life of just 0.26 nanoseconds, but that’s actually a long time in this business. The strange quark can only decay using the weak force, which, as its name suggests, is weak—so this happens slowly compared to decays involving the electromagnetic or strong forces.

For comparison, the Δ⁺ baryon is made of two ups and a down, just like a proton, but it has spin 3/2 instead of spin 1/2. So, you can think of it as a ‘fast-spinning proton’. It decays very quickly via the strong force: it has a mean life of just 5.6 × 10^-23 seconds! When you get used to things like this, a nanosecond seems like an eternity.

The unexpectedly long lifetime of the Λ and some other particles was considered ‘strange’, and this eventually led people to dream up a quantity called ‘strangeness’, which is not conserved, but only changed by the weak interaction, so that strange particles decay on time scales of roughly nanoseconds. In 1962 Murray Gell-Mann realized that strangeness is simply the number of strange quarks in a particle, minus the number of strange antiquarks.

So, what’s a ‘hypernucleus’?

A hypernucleus is nucleus containing one or more hyperons along with the usual protons and neutrons. Since nuclei are held together by the strong force, they do things on time scales of 10^-23 seconds—so an extra hyperon, which lasts for many billion times longer, can be regarded as a stable particle of a new kind when you’re doing nuclear physics! It lets you build new kinds of nuclei.

One well-studied hypernucleus is the hypertriton. Remember, an ordinary triton consists of a proton and two neutrons: it’s the nucleus of tritium, the radioactive isotope of hydrogen used in hydrogen bombs, also known as hydrogen-3. To get a hypertriton, we replace one of the neutrons with a Λ. So, it consists of a proton, a neutron, and a Λ.

In a hypertriton, the Λ behaves almost like a free particle. So, the lifetime of a hypertriton should be almost the same as that of a Λ by itself. Remember, the lifetime of the Λ is 0.26 nanoseconds. The lifetime of the hypertriton is a bit less: 0.24 nanoseconds. Predicting this lifetime, and even measuring it accurately, has taken a lot of work:

• Hypertriton lifetime puzzle nears resolution, CERN Courier, 20 December 2019.

Hypernuclei get more interesting when they have more protons and neutrons. In a nucleus the protons form ‘shells’: due to the Pauli exclusion principle, you can only put one proton in each state. The neutrons form their own shells. So the situation is a bit like chemistry, where the electrons form shells, but now you have two kinds of shells. For example in helium-4 we have two protons, one spin-up and one spin-down, in the lowest energy level, also known as the first shell—and also two neutrons in their lowest energy level.

If you add an extra neutron to your helium-4, to get helium-5, it has to occupy a higher energy level. But if you add a hyperon, since it’s different from both the proton and neutron, it can too can occupy the lowest energy level.

Indeed, no matter how big your nucleus is, if you add a hyperon it goes straight to the lowest energy level! You can roughly imagine it as falling straight to the center of the nucleus—though everything is quantum-mechanical, so these mental images have to be taken with a grain of salt.

One reason for studying hypernuclei is that in some neutron stars, the inner core may contain hyperons! The point is that by weaseling around the Pauli exclusion principle, we can get more particles in low-energy states, producing dense forms of nuclear matter that have less energy. But nobody knows if this ‘strange nuclear matter’ is really stable. So this is an active topic of research. Hypernuclei are one of the few ways to learn useful information about this using experiments in the lab.

For a lot more, try this:

• A. Gal, E. V. Hungerford and D. J. Millener, Strangeness in nuclear physics, Reviews of Modern Physics 88 (2016), 035004.

You can see some hyperons in the baryon octet, which consists of spin-1/2 baryons made of up, down and strange quarks:

and the baryon decuplet which consists of spin-3/2 baryons made of up, down and strange quarks:

In these charts I₃ is proportional to the number of up quarks minus the number of down quarks, Q is the electric charge, and S is the strangeness.

Gell-Mann and other physicists realized that mathematically, both the baryon octet and the baryon decuplet are both irreducible representations of SU(3). But that’s another tale!

Physics History Puzzle

Which famous physicist once gave a lecture attended by a secret agent with a pistol, who would kill him if he said the wrong thing?

Language Complexity (Part 4)

David A. Tanzer

Summarizing computational complexity

In Part 3 we defined, for each program P, a detailed function P'(n) that gives the worst case number of steps that P must perform when given some input of size n. Now we want to summarize P into general classes, such as linear, quadratic, etc.

What’s in a step?

But we should clarify something before proceeding: what is meant by a ‘step’ of a program? Do we count it in units of machine language, or in terms of higher level statements? Before, we said that each iteration of the loop for the ALL_A decision procedure counted as a step. But in a more detailed view, each iteration of the loop includes multiple steps: comparing the input character to ‘A’, incrementing a counter, performing a test.

All these interpretations are plausible. Fortunately, provided that the definition of a program step is ‘reasonable’, all of them will lead to the same general classification of the program’s time complexity. Here, by reasonable I mean that the definition of a step should be such that, on a given computer, there is an absolute bound on the amount of clock time needed for the processor to complete one step.

Approximately linear functions

The classification of programs into complexity classes such as linear, quadratic, etc., is a generalization which doesn’t require that the time complexity be exactly linear, quadratic, etc. For an example, consider the following code:

def approximately_linear(text):
    # perform a silly computation
    counter = 0
    for i = 1 to length(text):
        if i is odd:
            for j = 1 to 10:
                counter = counter + 1
    return counter
    

Here are the number of steps it performs, as a function of the input length:

f(0) = 2
f(1) = 13
f(2) = 14
f(3) = 25
f(4) = 26
f(5) = 37
...

The value increases alternately by 1 and then by 11. As it increases by 12 for every two steps, we could say that is “approximately linear,” with slope “roughly equal” to 6. But in fine detail, the graph looks like a sawtooth.

Soon, we will explain how this function gets definitively classified as having linear complexity.

Appendix: Python machines versus Turing machines

Here we are programming and measuring complexity on a Python-like machine, rather than a pure Turning machine. This is surfaced, for example, in the fact that without further ado we called a function length(text) to count the number of characters, and will regard this as a single step of the computation. On a true Turing machine, however, counting the length of the string takes N steps, as this operation requires that the tape be advanced one character at a time until the end of the string is detected.

This is a point which turns out not to substantially affect the complexity classification of a language. Assuming that steps are counted reasonably, any optimal decision procedure for a language of strings, whether written in Turing machine language, Python, C# or what have you, will end up with the same complexity classification.

The length function in Python really does take a bounded amount of time, so it is fair to count it as a single step. The crux of this matter is that, in a higher level language, a string is more than a sequence of characters, as it is a data structure containing length information as well. So there is order N work that is implied just by the existence of a string. But this can be folded into the up-front cost of merely reading the input, which is a general precondition for a language decider.

But, you may ask, what about languages which can be decided without even reading all of the input? For example, the language of strings that begin with the prefix “abc”. Ok, so you got me.

Still, as a practical matter, anything with linear or sub-linear complexity can be considered excellent and simple. The real challenges have do with complexity which is greater than linear, and which represents a real practical issue: software performance. So, for intents and purposes, we may treat any implied order N costs as being essentially zeros – as long as they can be on a one-time, up-front basis, e.g., the order N work involved in constructing a string object.

Reposted from the Signal Beat, Copyright © 2021, All Rights Reserved.

Theoretical Physics in the 21st Century

I’m giving a talk at the Zürich Theoretical Physics Colloquium next Monday, for Sustainability Week 2021. I’m excited to get a chance to speak both about the future of theoretical physics and the climate crisis. You can attend if you want.

Title: Theoretical Physics in the 21st Century

Time: Monday, 8 March 2021, 15:45 UTC (that is, Greenwich Mean Time).

Abstract: The 20th century was the century of physics. What about the 21st? Though progress on some old problems is frustratingly slow, exciting new questions are emerging in condensed matter physics, nonequilibrium thermodynamics and other fields. And most of all, the 21st century is the dawn of the Anthropocene, in which we will adapt to the realities of life on a finite-​sized planet. How can physicists help here?

Hosts: Niklas Beisert, Anna Knörr.

You can get a Zoom link here.

The Social Cost of Greenhouse Gases

Today the US government bumped the ‘social cost of greenhouse gases’ up to $51. The previous administration had knocked it down to between $1 and $7.

It’s a funny expression, ‘social cost of greenhouse gases’, but it means the marginal cost of the impacts caused by emitting one extra tonne of carbon dioxide—or the equivalent amount of any other greenhouse gas. This includes impacts on the environment and human health:

• Wikipedia, Social cost of carbon.

This new decision should affect US government policy decisions based on cost-benefit analyses:

For example, if the Trump administration had applied the Obama-era calculation to its rollback of federal mileage standards, the costs of that rule would have far outweighed the benefits and would have been much harder to justify. And any federal coal leasing in the Powder River Basin would be unlikely to win approval: University of Chicago professor Michael Greenstone noted that the climate damages associated with that mining “are six times larger than the market price of that coal.”

It may also wind up affecting decisions made by state and local governments and corporations. But it lags behind some states: in December 2020, New York adopted a ‘value of carbon guidance’ ranging between $79 and $125, depending on the discount rate assumed. The lower figure assumes a 3% annual discount of future damages, while the higher one assumes 2%.

The discount rate is crucial in all these calculations! The previous administration had reached its ludicrously low figure for the social cost of greenhouse gases using a couple of tricks: it neglected costs incurred outside the US, and it assumed a 7% annual discount rate. Biden’s new $51 cost assumes a 3% discount rate. At a 5% discount rate the cost would drop to merely $14.

All these calculations will be redone more carefully in a while:

While the Biden administration has set an initial price to inform its analysis of policies ranging from gas mileage standards to purchasing, it will embark on a months-long process to determine a longer-lasting one. That price will take other factors into account, such as the fact that the poor suffer more from climate impacts than the wealthy and more recent scientific findings on climate impacts.

The above quotes are from here:

• Juliet Eilperin and Brady Dennis, Biden is hiking the cost of carbon. It will change how the U.S. tackles global warming, Washington Post, 26 February 2021.

Here is today’s White House announcement on the social cost of carbon:

A Return to Science: Evidence-Based Estimates of the Benefits of Reducing Climate Pollution

On January 27, 2021, President Biden issued a Memorandum directing Federal agencies to make decisions guided by the best available science and data. Today, we are taking an important early step in bringing evidence-based principles back into the process of estimating the benefits of reducing climate pollution.

The evidence is clear that climate change is real and is already having economic consequences. The 2018 National Climate Assessment underscored the fact that climate change presents growing challenges to human health, safety, quality of life, and economic growth. We can see economic costs associated with climate change in more frequent and/or intense extreme weather events like wildfires, severe storms, and flooding, as well as the ways climate change disproportionately impacts the most vulnerable in society, particularly lower-income communities, communities of color, and Tribal communities. As decision-makers develop policies, they must incorporate the very real costs of climate change to current and future generations into their decisions.

One specific tool — called the “social cost of greenhouse gases” — combines climate science and economics to help Federal agencies and the public understand the benefits of reducing greenhouse gas emissions. The metric is a range of estimates, in dollars, of the long-term damage done by one ton of greenhouse gas emissions.

The use of this metric by the U.S. Government began in the Bush Administration and was later standardized across agencies in the Obama Administration. The Obama Administration created an Interagency Working Group of technical experts across the Federal Government to develop uniform estimates, subject to extensive public comment, in order to ensure that agencies utilized the best available science and economics.

However, the previous Administration disbanded the Interagency Working Group that had developed and refined these estimates and issued revised estimates based on assumptions that did not rely on the best available science or have the benefit of dedicated public comment. It also failed to implement 2017 recommendations from the experts at the National Academies of Sciences, Engineering, and Medicine that the Interagency Working Group had requested to ensure that these estimates continued to be in line with the latest science and economics.

This Administration will follow the science and listen to the experts. In a first-day executive order on Protecting Public Health and the Environment and Restoring Science To Tackle the Climate Crisis, President Biden reconvened the working group of technical experts from across the Federal Government and instructed them to restore the science- and economics-based approach to estimating climate damages.

The Interagency Working Group — co-chaired by the Office of Science and Technology Policy, Office of Management and Budget, and Council of Economic Advisers — today announced it is replacing the previous Administration’s estimates with the estimates developed prior to 2017, adjusted for inflation. This interim step will enable Federal agencies to immediately and more appropriately account for climate impacts in their decision-making while we continue the process of bringing the best, most up-to-date science and economics to the estimation of the social costs of greenhouse gases.

Today’s step restores three critical aspects of these estimates. First, the estimates put in effect today were subject to an extensive and robust process, including public notice and comment. A 2014 Government Accountability Office (GAO) report also concluded that the Interagency Working Group followed a “consensus-based” approach, relied on peer-reviewed academic literature, and disclosed relevant limitations when finalizing the estimates we are restoring today.

Second, these estimates take global damages into account. COVID-19 has re-emphasized the ways in which events on the other side of the globe can harm us here. Climate impacts abroad can affect the United States in many ways, including through supply chain disruptions, market volatility, and effects on our national security. In addition, climate actions taken by the United States and other countries under the Paris Agreement will benefit all countries, including the United States. Just as we expect and encourage other countries to consider the climate impact of their actions on us, we should take the global benefits of our actions into account.

Third, these estimates use the discount rates (the approach to calculating the present-day value of future climate damages) previously established by the Interagency Working Group. Restoring these rates puts these interim values in better alignment with the intergenerational nature of the climate challenge and the approaches taken in the peer-reviewed literature than the estimates used while the Interagency Working Group was disbanded.

A more complete update that follows the best science takes time. This is why we are quickly restoring the prior estimates as an interim step. With these estimates temporarily in place, the Interagency Working Group will continue its critical work to evaluate and incorporate the latest climate science and economic research and respond to the National Academies’ recommendations as we develop a more complete revision of the estimates for release within a year. Research, such as our understanding of the appropriate approach to discounting, has advanced rapidly over the past few years and we are collecting dedicated public comment through an upcoming Federal Register notice on how to improve our approach.

As this process proceeds, we are committed to engaging with the public and diverse stakeholders, seeking the advice of ethics experts, and working to ensure that the social cost of greenhouse gases consider climate risk, environmental justice, and intergenerational equity. The result will be even stronger science-based estimates developed through a transparent and robust process.

The Economics of Biodiversity

 

One problem with the Anthropocene is that our economic systems undervalue forms of “natural capital” for which there are no markets, or poorly developed markets. I’m talking about things like clean air, forests, wetlands, oceans… and biodiversity. For many of these things the price is zero or even negative, due to government subsidies.

So, we’ll burn through these things recklessly until the ensuing disasters wake us up. We’re like a family trying to earn more cash by selling off the windows and doors of our house. It may work for a while. But winter is coming.

Partha Dasgupta, an economist at the the University of Cambridge, has been studying this. In 2019, the UK government commissioned him to lead an independent, global review of the economics of biodiversity. It came out this month at an event hosted by the Royal Society and attended by the Prince of Wales, Boris Johnson and David Attenborough. Here it is:

• The Economics of Biodiversity: The Dasgupta Review.

The full report is 610 pages long. It’s very clear; I’m reading it and will say more about it here. There’s also a 103-page version and a 10-page ‘headline’ version, but the headlines leave out the really fun stuff: the economic analyses, the differential equations, and so on.

This came out at a good time for me, because I’ve recently been asked to give a talk about the economics of the Anthropocene. I seem to have reached the age where people ask me to give talks about practically anything I’ve ever blogged about. I need a lot of help on the economics, since I have intuitions but no framework to organize them. The Dasgupta Review provides a framework, and since I don’t have a lot of time before my talk, I plan to lean on it rather heavily.

Here’s the introduction, by David Attenborough. It’s easy to read. But it does not get into any of the economics, so please don’t judge the cake by its frosting.

We are facing a global crisis. We are totally dependent upon the natural world. It supplies us with every oxygen-laden breath we take and every mouthful of food we eat. But we are currently damaging it so profoundly that many of its natural systems are now on the verge of breakdown.

Every other animal living on this planet, of course, is similarly dependent. But in one crucial way, we are different. We can change not just the numbers, but the very anatomy of the animals and plants that live around us. We acquired that ability, doubtless almost unconsciously, some ten thousand years ago, when we had ceased wandering and built settlements for ourselves. It was then that we started to modify other animals and plants.

At first, doubtless, we did so unintentionally. We collected the kinds of seeds that we wanted to eat and took them back to our houses. Some doubtless fell to the ground and sprouted the following season. So over generations, we became farmers. We domesticated animals in a similar way. We brought back the young of those we had hunted, reared them in our settlements and ultimately bred them there. Over many generations, this changed both the bodies and ultimately the characters of the animals on which we depend.

We are now so mechanically ingenious that we are able to destroy a rainforest, the most species-rich ecosystem that has ever existed, and replace it with plantations of a single species in order to feed burgeoning human populations on the other side of the world. No single species in the whole history of life has ever been so successful or so dominant.

Now we are plundering every corner of the world, apparently neither knowing or caring what the consequences might be. Each nation is doing so within its own territories. Those with lands bordering the sea fish not only in their offshore waters but in parts of the ocean so far from land that no single nation can claim them. So now we are stripping every part of both the land and the sea in order to feed our ever-increasing numbers.

How has the natural world managed to survive this unrelenting ever-increasing onslaught by a single species? The answer of course, is that many animals have not been able to do so. When Europeans first arrived in southern Africa they found immense herds of antelope and zebra. These are now gone and vast cities stand in their stead. In North America, the passenger pigeon once flourished in such vast flocks that when they migrated, they darkened the skies from horizon to horizon and took days to pass. So they were hunted without restraint. Today, that species is extinct. Many others that lived in less dramatic and visible ways simply disappeared without the knowledge of most people worldwide and were mourned only by a few naturalists.

Nonetheless, in spite of these assaults, the biodiversity of the world is still immense. And therein lies the strength that has enabled much of its wildlife to survive until now. Economists understand the wisdom of spreading their investments across a wide range of activities. It enables them to withstand disasters that may strike any one particular asset. The same is true in the natural world. If conditions change, either climatically or as a consequence of a new development in the never-ending competition between species, the ecosystem as a whole is able to maintain its vigour.

But consider the following facts. Today, we ourselves, together with the livestock we rear for food, constitute 96% of the mass of all mammals on the planet. Only 4% is everything else – from elephants to badgers, from moose to monkeys. And 70% of all birds alive at this moment are poultry – mostly chickens for us to eat. We are destroying biodiversity, the very characteristic that until recently enabled the natural world to flourish so abundantly. If we continue this damage, whole ecosystems will collapse. That is now a real risk.

Putting things right will take collaborative action by every nation on earth. It will require international agreements to change our ways. Each ecosystem has its own vulnerabilities and requires its own solutions. There has to be a universally shared understanding of how these systems work, and how those that have been damaged can be brought back to health.

This comprehensive, detailed and immensely important report is grounded in that understanding. It explains how we have come to create these problems and the actions we must take to solve them. It then provides a map for navigating a path towards the restoration of our planet’s biodiversity.
Economics is a discipline that shapes decisions of the utmost consequence, and so matters to us all. The Dasgupta Review at last puts biodiversity at its core and provides the compass that we urgently need. In doing so, it shows us how, by bringing economics and ecology together, we can help save the natural world at what may be the last minute – and in doing so, save ourselves.

Native Type Theory

guest post by Christian Williams

Native Type Theory is a new paper by myself and Mike Stay. We propose a unifying method of reasoning for programming languages: model a language as a theory, form the category of presheaves, and use the internal language of the topos.

Though these steps are known, the original aspect is simply the composite and its application to software. If implemented properly, we believe that native types can be very useful to the virtual world. Here, I want to share some of what we’ve learned so far.

The Free Lunch

The biggest lesson of this paper was to have faith in what John Baez calls the dao of mathematics. For two years, Mike and I and Greg Meredith looked for ways to generate logics for programming languages; we tried many approaches, but ultimately the solution was the simplest.

Two facts of category theory provide an abundance of structure, for free:

1. Every category embeds into its presheaf topos.

2. Every topos has a rich internal language.

The embedding preserves limits and exponents, hence we can apply this to “higher-order theories”.

For now we explore the language of a topos. There are multiple views, and often its full power is not used. Toposes support geometric logic, predicate logic, and moreover dependent type theory. We emphasize the latter: dependent types are expressive and pervasive, yet underutilized in mathematics.

The Language of a Topos

My thinking has been shaped by the idea that even foundations are categorical. Virtually any language can be modelled as a structured category: the most comprehensive reference I’ve found is Categorical Logic and Type Theory by Bart Jacobs.

Probably the most studied categorical structure of logic is the topos. Toposes of sheaves, functors which coherently assign data to a space, were first applied to algebraic geometry. A continuous map induces an inverse image which is a left adjoint that preserves finite limits. This gives geometric morphisms of toposes, and geometric logic ( and ) as the language of classifying toposes.

Though geometric logic is an important level of generality, the language of toposes is more powerful. In La Jolla, California 1965, the budding category theory community recognized Grothendieck’s categories of sheaves as being fundamentally logical structures, which generalize set theory. An elementary topos is a cartesian closed category with finite limits and a subobject classifier, an object which represents the correspondence of predicates and subobjects.

The language of an elementary topos T is encapsulated in a pair of structures.

• The predicate fibration reasons about predicates, like subsets.

• The codomain fibration reasons about dependent types, like indexed sets.

Predicate Logic

Throughout mathematics, we use the internal predicate logic of Set. It is the canonical example of a topos: a predicate such as is a function , which corresponds to its comprehension, the subobject of true terms .

Predicates on any set form a Boolean algebra , ordered by implication. Every function gives an inverse image . This defines a functor which is a first-order hyperdoctrine: each has adjoints representing quantification, which satisfy the Beck–Chevalley condition.

Altogether, this structure formalizes classical higher-order predicate logic. Most formulae, such as

can be modelled in this logical structure of

This idea is fairly well-known; people often talk about the “Mitchell-Benabou language” of a topos. However, this language is predicate logic over a simple type theory, meaning that the only type formation rules are products and functions. Many constructions in mathematics do not fit into this language, because types often depend on terms:

This is provided by extending predicate logic with dependent types, described in the next section.

So, we have briefly discussed how the structure of Set allows for the the explicit construction of predicates used in everyday mathematics. The significance is that these can be constructed in any topos: we thereby generalize the historical conception of logic.

For example, in a presheaf topos , the law of excluded middle does not hold, and for good reason. Negation of a sieve is necessarily more subtle than negation of subsets, because we must exclude the possibility that a morphism is not in but “precomposes in” to a sieve. This will be explored more in the applications post.

Dependent Type Theory

Dependency is pervasive throughout mathematics. What is a monoid? It’s a set , and then operations on , and then conditions on . Most objects are constructed in layers, each of which depends on the ones before. Type theory is often regarded as “fancy” and only necessary in complex situations, similar to misperceptions of category theory; yet dependent types are everywhere.

The basic idea is to represent dependency using preimage. A type which depends on terms of another type, , can be understood as an indexed set , and this in turn is represented as a function . Hence the “world of types which depend on ” is the slice category .

The poset of “-predicates” sits inside the category of “-types”: a comprehension is an injection . This is a degenerate kind of dependent type, where preimages are truth values rather than sets. So we are expanding into a larger environment, which shares all of the same structure. The slice category is a categorification of : its morphisms are commuting triangles, understood as -indexed functions.

Every function gives a functor by pullback; this generalizes preimage, and can be expressed as substitution: given , we can form the -type

This functor has adjoints , called dependent sum and dependent product: these are the powerful tools for constructing dependent types. They generalize not only quantification, but also product and hom: the triple adjunction induces an adjoint co/monad on

These dependent generalizations of product and function types are extremely useful.

Indexed sum generalizes product type by allowing the type of the second coordinate to depend on the term in the first coordinate. For example: consists of dependent pairs .

Indexed product generalizes function type by allowing the type of the codomain to depend on the term in the domain. For example: consists of dependent functions .

See how natural they are? We use them all the time, often without realizing. Simply by using preimage for indexing, we generalize product and function types to “branching” versions, allowing us to build up complex objects such as

This rich language is available in any topos. I think we’ve hardly begun to see its utility in mathematics, computation, and everyday life.

All Together

A topos has two systems, predicate logic and dependent type theory. Each is modelled by a fibration, a functor into the topos for which the preimage of are the -predicates / -types. A morphism in the domain is a judgement of the form “in the context of variables of these (dependent) types, this term is of this (dependent) type”.

The two fibrations are connected by comprehension which converts a predicate to a type, and image factorization which converts a type to a predicate. These give that the predicate fibration is a reflective subcategory of the type fibration.

Altogether, this forms the full higher-order dependent type theory of a topos (Jacobs Ch.11). As far as I know, this is what deserves to be called “the” language of a topos, in its full glory. This type theory is used in proof assistants such as Coq and Agda; eventually, this expressive logic + dependent types will be utilized in many programming languages.

Conclusion

Native Type Theory gives provides a shared framework of reasoning for a broad class of languages. We believe that this could have a significant impact on software and system design, if integrated into existing systems.

In the next post, we’ll explore why this language is so useful for the topos of presheaves on theories. Please let me know any thoughts or questions about this post and especially the paper. Thank you.

Language Complexity (Part 3)

David A. Tanzer

A detailed measure of computational complexity

In Part 2, we identified language complexity by how “difficult” it is for a program to decide if some given text is a sentence of the language — in other words, by the complexity of the decision problem for the language.  

Note there may be many decision procedures — which are implementations of functions — that solve the decision problem for a language. For our purposes, we will focus our attention just on the ones which give the best performance. As motivation for this focus, consider that our simple language ALL_A = {“A”, “AA”, “AAA”, …} could be decided by an ill-conceived program which does all sorts of unnecessary work — but that would say nothing about the complexity of ALL_A itself. On the other hand, the procedure which simply scans the characters and verifies that all are ‘A’ is optimal, and simple — which shows that ALL_A is itself a simple language.

Our goal now is to quantify the notion of language complexity. That boils down to the matter of how to quantify the amount of work a program — in this case, the language decider — needs to do.

Computational complexity

Say we have a program P that inputs a string, goes through some steps, and outputs some results. For each input string, we can count how many computation steps it leads to.   Let StepCount(P,x) be the number of steps needed to compute the result from x.

Now let’s consider the effect of the size of the input on the number of steps. 

In general, we expect larger inputs to trigger longer sequences of computation steps. In the first place, it takes more steps to scan more text. And moreover, as the analysis gets larger, more steps will be involved.

Checking whether all characters are ‘A’ takes order N work, where N is the size of the input string.

For something that requires more than order N work, consider a program which takes as input the text representation of a number, parses it, and computes the number of factors in the number. The analysis of factors calls for a significant amount of computation beyond the N steps to scan the input. Moreover, this work will become larger and more complex as the input values become larger.

These facts are indicators of what is known as the time complexity of the computation.

Sidenote: the space complexity of a computation pertains to the amount of memory it uses, as a function of input size. In our context, we are considering just the time complexity, i.e., the running time as a function of input size.

Worst-case complexity

It is fair to ask what is meant by the number of computation steps required to compute the output, for input of size N. After all, there are multiple input strings of size N, each of which may trigger a different number of computation steps. For instance, take our loop-based decision procedure for ALL_A. Input “AAAAA” causes 5 computation steps (as the loop runs through to completion). But “AABAA”, also of length 5, causes only 3 computation steps (as the loop terminates once it sees the ‘B’).

What we care about here is just the maximum number of steps that will be needed for a given input size. In other words, we focus our analysis on the worst-case behavior for each input size N. The motivation here is that any bound on running time that we put on the worst-case inputs of size N gives us a bound for all inputs of size N.

Let MaxSteps(P,N) be the maximum number of steps that program P may perform for an input of size N.

Let P'(N) = MaxSteps(P,N).

So P’ is the function that gives us the maximum number of steps that P will perform for any input size N.

P’ is our first step towards quantifying the time complexity of the program P. 

But for typical purposes, P’ presents an overly detailed description of complexity.

For instance, take a decision procedure P for ALL_A. We would like to be able to summarize the time complexity of P by saying that it is linear in the size of the input string. That information is contained in the structure of the function P'(n). But P’ offers a much more granular description, with one value for every natural number n.

In the next posts we will look into the classification of P'(n) into general complexity classes such as linear, quadratic and exponential.

Reposted from the Signal Beat, Copyright © 2021, All Rights Reserved.

Talc

 

Talc is one of the softest minerals—its hardness defines a ‘1’ on Moh’s scale of hardness. I just learned its structure at the molecular level, and I can’t resist showing it to you.

Talc is layers of octahedra sandwiched in tetrahedra!

Since these sandwiches form separate parallel sheets, I bet they can easily slide past each other. That must be why talc is so soft.

The octahedra are magnesium oxide and the tetrahedra are silicon oxide… with some hydroxyl groups attached to liven things up. The overall formula is Mg₃Si₄O₁₀(OH)₂. It’s called ‘hydrated magnesium silicate’.

The image here was created by Materialscientist and placed on Wikicommons under a Creative Commons Attribution-Share Alike 3.0 Unported license.

Serpentine Barrens

 

This is the Soldiers Delight Natural Environmental Area, a nature reserve in Maryland. The early colonial records of Maryland describe the area as a hunting ground for Native Americans. In 1693, rangers in the King’s service from a nearby garrison patrolled this area and named it Soldiers Delight, for some unknown reason.

It may not look like much, but that’s exactly the point! In this otherwise lush land, why does it look like nothing but grass and a few scattered trees are growing here?

It’s because this area is a serpentine barrens. Serpentine is a kind of rock: actually a class of closely related minerals which get their name from their smooth or scaly green appearance.

Soils formed from serpentine are toxic to many plants because they have lots of nickel, chromium, and cobalt! Plants are also discouraged by how these soils have little potassium and phosphorus, not much calcium, and too much magnesium. Serpentine, you see, is made of magnesium, silicon, iron, hydrogen and oxygen.

As a result, the plants that actually do well in serpentine barrens are very specialized: some small beautiful flowers, for example. Indeed, there are nature reserves devoted to protecting these! One of the most dramatic is the Tablelands of Gros Morne National Park in Newfoundland:

Scott Weidensaul writes this about the Tablelands:

These are hardly garden spots, and virtually no animals live here except for birds and the odd caribou passing through. Yet some plants manage to eke out a living. Balsam ragwort, a relative of the cat’s-paw ragwort of the shale barrens, has managed to cope with the toxins and can tolerate up to 12 percent of its dry weight in magnesium—a concentration that would level most flowers. Even the common pitcher-plant, a species normally associated with bogs, has a niche in this near-desert, growing along the edges of spring seeps where subsurface water brings up a little calcium. By supplementing soil nourishment with a diet of insects trapped in its upright tubes, the pitcher-plant is able to augment the Tablelands’ miserly offerings. Several other carnivorous plants, including sundews and butterwort, work the same trick on their environment.

In North America, serpentine barrens can be found in the Appalachian Mountains—Gros Morne is at the northern end of these, and further south are the Soldiers Delight Natural Environmental Area in Maryland, and the State Line Serpentine Barrens on the border of Maryland and Pennsylvania.

There are also serpentine barrens in the coastal ranges of California, Oregon, and Washington. Here are some well-adapted flowers in the Klamath-Siskiyou Mountains on the border of California and Oregon:

I first thought about serpentine when the Azimuth Project was exploring ways of sucking carbon dioxide from the air. If you grind up serpentine and get it wet, it will absorb carbon dioxide! A kilogram of serpentine can dispose about two-thirds of a kilogram of carbon dioxide. So, people have suggested this as a way to fight global warming.

Unfortunately we’re putting out over 37 gigatonnes of carbon dioxide per year. To absorb all of this we’d need to grind up about 55 gigatonnes of serpentine every year, spread it around, and get it wet. There’s plenty of serpentine available, but this is over ten times the amount of worldwide cement production, so it would take a lot of work. Then there’s the question of where to put all the ground-up rock.

And now I’ve learned that serpentine poses serious challenges to the growth of plant life! It doesn’t much matter, given that nobody seems eager to fight global warming by grinding up huge amounts of this rock. But it’s interesting.

Credits

The top picture of the Soldiers Delight Natural Environmental Area was taken by someone named Veggies. The picture of serpentine was apparently taken by Kluka. The Tablelands were photographed by Tango7174. All these are on Wikicommons. The quote comes from this wonderful book:

• Scott Weidensaul, Mountains of the Heart: A Natural History of the Appalachians, Fulcrum Publishing, 2016.

The picture of flowers in the Klamath-Siskiyous was taken by Susan Erwin and appears along with many other interesting things here:

• Klamath-Siskiyou serpentines, U. S. Forest Service.

A quote:

It is crystal clear when you have entered the serpentine realm. There is no mistaking it, as the vegetation shift is sharp and dramatic. Full-canopied forests become sparse woodlands or barrens sometimes in a matter of a few feet. Dwarfed trees, low-lying shrubs, grassy patches, and rock characterize the dry, serpentine uplands. Carnivorous wetlands, meadows, and Port-Orford-cedar dominated riparian areas express the water that finds its way to the surface through fractured and faulted bedrock.

For more on serpentine, serpentinization, and serpentine barrens, try this blog article:

• Serpentine, Hiker’s Notebook.

It’s enjoyable despite its misuse of the word ‘Weltanschauung’.