Wednesday, April 20, 2016

TikZ (PGF) Packages


I haven't found an up-to-date list of packages that use/support the wonderful PGF/TikZ library, so I went through the latex packages in the latest TexLive and found these.  It's not exhaustive but it's better than nothing.  I excluded some libraries that use pgf/tikz under the covers (e.g. chemmacros).

PGF/TikZ

  • aobs-tikz  -  overlayed pictures in beamer
  • bloques -  control blocks
  • blox - block diagrams
  • bondgraphs - 
  • braids - braid diagrams
  • celtic - celtic-style knots
  • circuitikz - electrical and electronic networks.  NB: tikz 3.0.1a has builtin support for some circuit libraries that was inspired by this library.
  • csvsimple - uses key-value syntax from pgfkeys
  • diadia - diabetes diary
  • endiagram - potential energy curve diagrams
  • forest - linguistic trees
  • hf-tikz  -  highlight formulas
  • hobby - a tikzlibrary implementing John Hobby's algorithm for cubic bezierz curves
  • makeshape - method of creating custom shapes in PGF
  • mframed  - Framed environments that can split at page boundaries
  • ocgx - Optional Content Group support (layers)
  • pgf-blur - blurred shadows
  • pgf-soroban
  • pgf-umlcd
  • pgf-umlsd
  • pgfgantt
  • pgfkeyx
  • pgfopts
  • pgfornament
  • pgfplots
  • prooftrees  -  based on forest
  • sa-tikz "a library to draw switching architectures"
  • spath3
  • tikz-3dplot
  • tikz-cd  -  commutative diagrams
  • tikz-dependency - dependency diagrams for linguistics
  • tikz-dimline  -  technical dimension lines (e.g. showing a widget is 4cm wide, etc)
  • tikz-feynman
  • tikz-inet  -  interaction nets
  • tikz-opm  -  Object Process Methodology diagrams
  • tikz-plattice  -  particle accelerator lattices
  • tizk-qtree -  2012.  NB: tikz 3.0.1a (and maybe earlier) has extensive built-in support for trees
  • tikz-timing - timing diagrams
  • tikzinclude - importing images
  • tikzmark  -  mark a point in a page for further use
  • tikzorbital - molecular diagrams
  • tizkpagenodes - extending current page nodes
  • tikzpfeile  -  arrows
  • tikzposter - generate scientific posters
  • tikzscale - absolute resizing
  • tikzsymbols - great collection of symbols that started with cookbook symbols and then grew
  • tkz-orm - Object-Role Model drawing.  NB: *not* part of the TKZ collection.
  • visualtikz - excellent visual documentation for tikz: extensive collection of simple examples showing syntax and result

The Altermundus TKZ Collection


This collection of PGF/TikZ libraries by the prolific Alain Matthes is so awesome it deserves its own section.  Some of the documentation is in French only.  (Note the spellings, tkz v. tikz)
  • alterqcm  -  two-column multiple choice questions  (Fr)
  • tizkrput - macro for placing stuff
  • tkz-base
  • tkz-berge - graphs (En)
  • tkz-euclide - an amazing library for doing good old fashioned geometry.   The doc is in French but if you know TikZ you can probably figure it out; if not, its a very good reason to learn French.
  • tkz-fct - 2d function plotting
  • tkz-graph  - more graphs (Fr)
  • tkz-linknodes - links between lines of an environment (En)
  • tkz-kiviat
  • tkz-tab  -  very fancy table support (Fr)
  • tkz-tukey

Monday, April 11, 2016

Developer-friendly IoT devices and tools


IoT Overview:
Devices:
  • Arduino/Genuino 101 - the new Arduino uses the Intel Curie!  See also the Intel Arduino101 site.
  • ESP8266  This is a very impressive and cheap little IoT device - MCU, WIFI, etc. for a couple of bucks!  Breakout modules for anywhere from $6 to $10.  Do a web search and you'll find lots of ESP8266 info and products; a good place to start is esp8266.com.  Support for Lua and Javascript.  CAVEAT: the ESP8266 has already been through numerous versions so make sure you get the one you want.
  • Intel Edison - a little more expensive but a lot more powerful - a CPU running Linux, a separate MCU, a DSP, Wifi, Bluetooth, lots of memory, etc.
  • Texas Instruments has tons of IoT stuff.  Look for the Launchpad for the device you're interested in - these are inexpensive Arduino-like dev boards that make it easy to tinker.  The website also has lots of background info, whitepapers, training vids, etc.  See in particular
  • OpenMote
  • Other HW vendors: the semiconductor market is very competitive, with many major players and heaven knows how many smaller ones. Many of them are beginning to offer Arduino-like development boards for products that previously would only have been of interest to professional EEs.  See for example:
    • NXP - Formerly Philips Semiconductor.  NXP recently acquired Freescale, which was formerly the semiconductor division of Motorola
    • Atmel - recently acquired by Microchip.  Up until the release of the Arduino101, which uses the Intel Curie MCU, Arduinos used Atmel MCUs
    • STMicroelectronics
  • Online IoT-friendly retailers: lots.  I've had good luck with these, but there are lots of others; do shop around.
  • Make - maker zine
  • Hackster.io

Software:
  • Espruino
  • NodeMCU "open-source firmware and development kit that helps you to prototype your IOT product within a few Lua script lines"  (ESP8266)
  • AT&T Flow - web-based dev environment.  based on:
  • Node-RED - "A visual tool for wiring the Internet of Things" (developed and open-sourced by IBM)
  • Alljoyn
  • Iotivity
Operating Systems:
Protocols:
Standards:
Standards bodies:

Cloud services - testing, data storage, etc.

  • IoT-LAB  "IoT-LAB provides a very large scale infrastructure facility suitable for testing small wireless sensor devices and heterogeneous communicating objects."

Other:
  • awesome-iot - a list of IoT resources somebody put on github
  • IPSO Alliance page listing devices for building smart objects

Saturday, March 19, 2016

Coinduction Resources

Here are some materials I've found useful in trying to understand coinduction and related notions. Most of them involve some pretty heavy mathematics, but their introductions usually provide an overview and some examples that will help you develop your intuitions even if the math is over your head.

Some major figures, all of whom have made many publications available on their homepages:


A good place to start is An introduction to (co)algebra and (co)induction (PDF) by Rutten and Jacobs. (in Advanced Topics in Bisimulation and Coinduction).  The first part gives several concrete examples that will help you understand coinduction.

Coinductive Models of Finite Computing Agents by Wegner and Goldin.  Free version available on their homepages.

Communicating and Mobile Systems: the Pi Calculus, Milner.  Not easy to read, but well worth the effort.

An interesting paper showing how the concepts of bisimulation and bisimilarity emerged independently in computer science, philosophical logic, and set theory:  On the Origins of Bisimulation and Coinduction, Sangiorgi.  Free version available on author's homepage.

Universal coalgebra: a theory of systems, Rutten.  A landmark paper, I gather.  You can find a free version on Rutten's homepage.

Coalgebraically Thinking, David Corfield (blog post, n-Category Cafe, 2008)

This seems to be a growth industry; a number of introductory texts have been published in the past few years:


Friday, March 11, 2016

The Problem with Inductive Definition - and why it needs coinductive codefinition

There's a subtle problem with inductive definitions.  Consider the cannonical example of Nat, usually defined using something like the following pseudo-code:

Nat: Type
Z : Nat
S : Nat -> Nat

The problem is that given only this definition we cannot answer a simple question:  is every n:Nat of the form S...Z?  In other words, do the cannonical constructors of an inductively defined type exhaust the membership of that type?

The mathematician Andrej Bauer wrote an interesting blog post on this topic (The elements of an inductive type), but he comes at it from a very different perspective than I do.  His focus is on models of Nat, and he shows that there are various "exotic" models, which he describes thusly:  "Let us call a model exotic if not every element of (the interpretation of) 𝚗𝚊𝚝 is obtained by finitely many uses of the successor constructor, starting from zero."  It's an interesting post (as are the comments), but I think it misses the key point, which is that the problem is inherent in the structure of inductive definition; models are beside the point.  In this article I take a stab at an alternative characterization of the problem and a possible solution.

The reason we cannot answer the question of whether an inductively defined type contains only those elements built up using the constructors, given only the inductive definition, is that the inductive part of the definition (here, S) makes the assumption that its argument is of the appropriate type, but that's the only assumption it makes.  In particular it makes no assumption as to the structure of that argument. We can make this a bit more explicit using informal English:

Z is a natural number
Assuming that n is a natural number, infer that Sn is a natural number.

So we've assumed that n:Nat, but we have not assumed that it has cannonical form.  Maybe it was constructed solely using Z and S, maybe it wasn't - all we know (or rather assume) is that it is a Nat. For the purposes of inductive definition, it does not matter: S is a rule. If n is in fact of type Nat (no assumption here), then, no matter what its form or how we got it, Sn is of type Nat, end of story.  So for all we know, Nat could be chock-full of non-canonical members.

That's not very satisfactory, since intuition tells us that of course there is nothing in Nat that is not constructed from Z and S.  But our inductive definition does not say this, and there is no way to prove it from the definition alone.

Then how can we vindicate our intuitions, and show that every Nat is built up using nothing but S, starting from Z?  We want something like the following proposition:

For all n:Nat, either n=Z or n=Sm for some m:Nat   ;; where n=Sm means Sm is the canonical form of n)

Note that the inductive definition of Nat does not justify the second part of this proposition.  It tells us that every n:Nat has a successor Sn:Nat, but it does not tell us that every n:Nat is the successor to some other Nat (that is, has a predecessor "some m" such that n=Sm).  Even worse, it leaves open the possibility that every n:Nat could have any number of predecessors.  It may seem intuitively obvious that every Nat has a unique successor and a unique predecessor, but again, the definition does not say this; in fact it does not even imply it if your intuition hasn't already been trained to expect it.  Nor can it be used to prove it.

We cannot justify this inductively, since induction will always involve assumptions as above, and if we try to build canonicity into our assumptions we just move the problem.  For example it won't work to say "Assuming that n is either Z or a Nat of form Sm, then Sn is a Nat", since the same problem arises with respect to m.  And we cannot go further and say "Assuming that n is a cannonical Nat..." because that is obviously circular - you only get canonical form after you've defined S.

The only way I can see to do it is to use the dual notion of coinduction.  The idea is that we can introduce another operator P (Predecessor) and use it to show that every n:Nat can be expressed as (or reduced to, or equivalent to,  choose your terminology) a canonical form.  But not: defined as a canonical form!  Coinduction does not define; it does not say what things are (no metaphysics here); rather, it characterizes how they behave, which is to say it codefines them.  (See my previous post, Definition and Co-definition, for more on the distinction.)  The fact that every n:Nat has a predecessor (with PZ = Z) does not define Nat, it just says what you can do with a Nat once you have one.  By the same token it is not quite true to say that Z and S define Nat; they define those elements of Nat that have canonical form, but they do not "close" Nat, in that they do not and cannot exclude the possibility of (undefined) non-canonical Nat forms.

So to get a complete and intuitively satisfying "definition" of Nat we need both an inductive definition of canonical forms and a coinductive codefinition of non-canonical forms.  Here's one way to get started that I don't think works:

P :  Nat -> Nat

Leaving aside the fact that this just looks like an alias for S (I'll address that problem in a minute), the form of this expression obscures the difference between inductive constructor and coinductive coconstructor.  Informally, an inductive constructor of a type X takes things "into" X; a coinductive coconstructore takes things "from" X.  We can therefore make this structure more conspicuous as follows:

S : Nat -> X
P : Nat <- X

and setting X == Nat.  We could also have written P : X -> Nat, but that would make P look like a constructor for Nat rather than a coconstructor for X.  It's really the reversal of the arrow that exposes the duality, rather than the swapping of the type variables.

So now we have P: Nat <- X, but that just looks like a funny way to write S.  All it says is that if you have n:Nat, then you have Pn:Nat.  Now the question is how to express the idea that P functions as a predecessor operation.  The only way to do that is in terms of S.

PZ = Z
SPn = Sn ;; n = Z
SPn = n   ;; n != Z

Note that we are not using S to define P.  That is, we do not want to define P by saying P(Sn) = n; we want instead to start with the same minimal assumption we used to specify S, namely, "Assuming n:Nat, infer Pn...".  In fact we're not really defining P at all!  Instead we're specifying the relation between S and the result of using P. There's really nothing in this "definition" that characterizes P as a predecessor operation, except for the fact that the successor operation S cancels it out.  In a sense the operation P performs is completely hidden, and could be anything; all that matters is that once you use P, you can use S to cancel it out.

(Note that S : Nat -> X is also not a definition of S.  It does not define any mechanism, operation, algorithm, etc. that S performs.  Constructors like S, and coconstructors like P, are not functions.)

This definition/codefinition answers our original question directly.  Every n:Nat is equal to S(Pn), which is in canonical form.

I haven't said much about what coinduction really is, or why we should think of P as a coconstructor, etc.  I'll address that in another post.

(Aside:  some writers define "canonical form" as a form containing only canonical constructors, e.g. SSSZ; others defined it as one whose outermost form is a canonical constructor, e.g. Sn is in canonical form.)