The Solar Impulse 2 aircraft has begun its solar-powered trans-Pacific crossing. Track the aircraft on its 5-day leg to Hawaii on www.flightradar24.com/SOLAR2, see telemetry data at www.solarimpulse.com/rtw, or follow the journey with @solarimpulse on Twitter. Bon voyage, team!
Because of a gap in 2013, I had forgotten about the Wellcome Image Awards. This SEM image of a kidney stone by Kevin Mackenzie was one of the winning entries for 2014:
So was this strangely beautiful SEM image of sludge from an industrial farming process by Eberhardt Josué Friedrich Kernahan and Enrique Rodríguez Cañas:
This SEM image of a Purkinje cell by Michael Häusser, Sarah Rieubland, and Arnd Roth was one of this year’s winners:
So was this micro-computed tomography scan of the skull and front legs of a tuatara (a New Zealand reptile) by Sophie Regnault:
And this illustration of pollen grains being released from the anther of a flower by Maurizio De Angelis:
All images used under Creative Commons license (CC BY-NC-ND). Click images to zoom and/or read more about the pictures. They’re lovely, don’t you think?
It was Eurovision again on the weekend. This time, Australia competed. And voted – twice. Officially, during the contest; and in the Australian evening, unofficially, at sbs.com.au.
I have no time for the kind of analyses I did last year but, as the graph below shows, the unofficial Australian percentage ratings tracked the official Eurovision scores reasonably well (with substantial random variation), except for the huge vote for home:
I have previously blogged about carbon dating, a method which can be used to date organic items up to about 50,000 years old. Tests of carbon-dating have used tree-ring data back to around 10,000 BC.
The timeline above shows some highlights of the past 30,000 years, including one of the oldest cities, the oldest living tree, the oldest pyramid, and a Babylonian clay tablet I blogged about two years ago. The two caves in France are definitely on my “bucket list.”
NetLogo programs sometimes require agents to reason, and one of the simplest forms of reasoning is the sequent calculus. This uses expressions of the form α, β, γ, δ ⊢ ε, ζ, η which are interpreted as α ˄ β ˄ γ ˄ δ ⇒ ε ˅ ζ ˅ η. That is, all the hypotheses α, β, γ, δ are assumed to be true, and from that it should follow that at least one of the conclusions ε, ζ, η is true.
We can resolve the truth of sequents like α, β, γ, δ ⊢ ε, ζ, η using rules which simplify occurrences of ¬ φ (not φ), φ ˄ ψ (φ and ψ), φ ˅ ψ (φ or ψ), and φ ⇒ ψ (φ implies ψ) occurring in the hypotheses and/or conclusions, until we are left with a number of sequents like α, β, γ, δ ⊢ ε, ζ, η containing only atomic formulae. Such an expression is true if one of the atomic formulae on the left also occurs on the right (or, in more advanced versions of the logic, if the atomic formulae on the left somehow imply one of the atomic formulae on the right, in the way that x = y and y = z imply x = z).
The simplification rules are as follows. Note that some rules generate two new sequents, and that the rule for not flips things from the hypotheses to the conclusions or vice versa:
We can code these up easily in NetLogo, using the list [ "and" φ ψ ] to represent φ ˄ ψ, and so forth. The following function takes 4 lists (atomic and non-atomic hypotheses; atomic and non-atomic conclusions) and applies the simplification rules to the hypotheses (with some printing for debugging):
to-report sequent-prove-a [ atomic-hyp non-at-hyp atomic-conc non-at-conc ] ; split hypotheses
nice-print "a" atomic-hyp non-at-hyp atomic-conc non-at-conc ""
ifelse (non-at-hyp = [])
[ report sequent-prove-b atomic-hyp atomic-conc non-at-conc ]
[ let p (first non-at-hyp)
set non-at-hyp (but-first non-at-hyp)
ifelse (is-string? p) ; atomic
[ report sequent-prove-a (fput p atomic-hyp) non-at-hyp atomic-conc non-at-conc ]
[ ifelse (first p = "not") ; not q
[ let q (item 1 p)
report sequent-prove-a atomic-hyp non-at-hyp atomic-conc (fput q non-at-conc) ]
[ ifelse (first p = "and") ; q /\ r
[ let q (item 1 p)
let r (item 2 p)
report sequent-prove-a atomic-hyp (fput q (fput r non-at-hyp)) atomic-conc non-at-conc ]
[ ifelse (first p = "or") ; q \/ r
[ let q (item 1 p)
let r (item 2 p)
report (sequent-prove-a atomic-hyp (fput q non-at-hyp) atomic-conc non-at-conc)
and (sequent-prove-a atomic-hyp (fput r non-at-hyp) atomic-conc non-at-conc) ]
[ ifelse (first p = "implies") ; same as (not q) \/ r
[ let q (item 1 p)
let r (item 2 p)
report (sequent-prove-a atomic-hyp (fput r non-at-hyp) atomic-conc non-at-conc)
and (sequent-prove-a atomic-hyp non-at-hyp atomic-conc (fput q non-at-conc)) ]
[ error "Unexpected logical" ]
]
]
]
]
]
endOnce all hypotheses are atomic, the following function applies the simplification rules to the conclusions (for some cases it must call sequent-prove-a again):
to-report sequent-prove-b [ atomic-hyp atomic-conc non-at-conc ] ; split conclusions
nice-print "b" atomic-hyp [] atomic-conc non-at-conc ""
ifelse (non-at-conc = [])
[ report sequent-prove-c atomic-hyp atomic-conc ]
[ let p (first non-at-conc)
set non-at-conc (but-first non-at-conc)
ifelse (is-string? p) ; atomic
[ report sequent-prove-b atomic-hyp (fput p atomic-conc) non-at-conc ]
[ ifelse (first p = "not") ; not q
[ let q (item 1 p)
report sequent-prove-a atomic-hyp (list q) atomic-conc non-at-conc ]
[ ifelse (first p = "and") ; q /\ r
[ let q (item 1 p)
let r (item 2 p)
report (sequent-prove-b atomic-hyp atomic-conc (fput q non-at-conc))
and (sequent-prove-b atomic-hyp atomic-conc (fput r non-at-conc)) ]
[ ifelse (first p = "or") ; q \/ r
[ let q (item 1 p)
let r (item 2 p)
report sequent-prove-b atomic-hyp atomic-conc (fput q (fput r non-at-conc)) ]
[ ifelse (first p = "implies") ; same as (not q) \/ r
[ let q (item 1 p)
let r (item 2 p)
report sequent-prove-a atomic-hyp (list q) atomic-conc (fput r non-at-conc) ]
[ error "Unexpected logical" ]
]
]
]
]
]
endOnce both hypotheses and conclusions are atomic, checking truth just needs a simple intersection test:
to-report sequent-prove-c [ atomic-hyp atomic-conc ]
let proved? false
foreach atomic-conc [
if ((not proved?) and member? ? atomic-hyp) [ set proved? true ]
]
ifelse (proved?)
[ nice-print " c" atomic-hyp [] atomic-conc [] " ** proved **" ]
[ nice-print " c" atomic-hyp [] atomic-conc [] " failed!" ]
report proved?
endPrinting requires some code to make sequents look nice:
to-report nice-item [ p ]
ifelse (is-string? p)
[ report p ]
[ ifelse (first p = "not")
[ let q (item 1 p)
report (word "~ " (nice-item q)) ]
[ ifelse (first p = "and")
[ let q (item 1 p)
let r (item 2 p)
report (word "(" (nice-item q) " ^ " (nice-item r) ")") ]
[ ifelse (first p = "or")
[ let q (item 1 p)
let r (item 2 p)
report (word "(" (nice-item q) " v " (nice-item r) ")") ]
[ ifelse (first p = "implies")
[ let q (item 1 p)
let r (item 2 p)
report (word "(" (nice-item q) " -> " (nice-item r) ")") ]
[ error "Unexpected logical" ]
]
]
]
]
end
to-report nice-list [ p ]
ifelse (p = [])
[ report "" ]
[ report (reduce [ (word ?1 ", " ?2) ] (map nice-item p)) ]
end
to nice-print [ lab x y z w t]
if (verbose?) [
print (word lab ": " (nice-list (sentence x y)) " |- " (nice-list (sentence z w)) t)
]
endFor demonstration purposes, the go button computes some basic facts about two turtles, combining this with a user-supplied list of hypotheses, and tries to prove a user-supplied conclusion (in this case [ "and" [ "implies" "C" "F" ] [ "not" [ "not" "Far" ] ] ], representing (C ⇒ F) ˄ ¬ ¬ Far.
globals [
computed-facts
result?
]
to go
if (verbose?) [ print "------------------------------------------------------------------------" ]
clear-all
ask patches [ set pcolor white ]
create-turtles 1 [ set color blue set size 3 set shape "person" setxy random-xcor random-ycor ]
create-turtles 1 [ set color red set size 2 set shape "person" setxy random-xcor random-ycor ]
set result? "?"
ask (turtle 0) [ compute-basic-facts ]
let hypotheses (sentence computed-facts (read-from-string other-hypotheses))
set result? sequent-prove-a [] hypotheses [] (list (read-from-string conclusion))
end
to compute-basic-facts ; calculated by a specific turtle
let fact1 (ifelse-value (xcor < 0) [ "Left" ] [ "Right" ])
let d (distance (turtle 1))
let fact2 (ifelse-value (d < 4) [ "Near" ] [ "Far" ])
set computed-facts (list fact1 fact2)
endThe NetLogo interface is shown at the top of this page, and the code is at Modelling Commons. The simple sequent calculus reasoner presented here can be fairly easily extended with quantifiers and other features that might be necessary.
See also my other NetLogo tutorials.
National Science Week in Australia is here in three months. Plenty of time to think up and register an event.
You can also read a science book or visit a museum. So why not take part?
Today, some pretty pictures from recent photographic competitions. First, the European Geosciences Union Photo Contest 2014. “Erosion Spider” by John Clemens was one of the winning entries:
Second, the BioMedCentral Ecology Image Competition. “A sticky snack for mice” by Petra Wester was the overall winner:
Finally, the Neuro Bureau Brain Art Competition 2014. “Heart of the Brain” by Chris Steele (MPI Leipzig) won the Best Visualization of Probabilistic Connectivity category:
All images used under Creative Commons license (CC BY-NC-ND, CC BY, and CC BY-NC-SA respectively). Click images to zoom and/or read more about the photographs.
The Dawn spaceprobe, now orbiting the dwarf planet Ceres, took the lovely photograph above a few days ago (image credit: NASA/JPL-Caltech/UCLA/MPS/DLR/IDA). Click the image to zoom.
And here is a NASA/JPL-Caltech artist’s concept of Dawn’s ion thrusters in action. The xenon ions glow blue:
Meanwhile, the New Horizons spaceprobe is getting closer and closer to Pluto:
This means the pictures are getting better. As New Horizons looks towards Pluto and Charon, we are starting to see hints of surface features:
We can even see colours, although the pictures are still very fuzzy:
Scientific Gems 