A fragment of the FORMEL Library

In 1988 I was a guest of the FORMEL Project at INRIA, as a wandering ABD.  The forte of FORMEL was the unification algorithm, and I spent some time copying papers from a filing cabinet which, after my time, grew to be 3 or 4 filing cabinets and became known as the Formel Library.  I hear that, as the project disbanded, the cabinets were donated to another institution and then subsequently lost.  I copied 56 papers from the library and put them into 5 themed binders.  Recently I was possessed of a desire to clean out a storage space I have been renting, to save money by giving back the space.  The storage space is filled with items I can’t part with and never consult, including those 5 binders.

The obvious thing to do would be to scan and upload all of the papers to something like ResearchGate.  However, this thought was nixed by the Academia StackExchange community.  But what if there was something rare, valuable and irreplaceable in my collection?  Well, I inventoried what I had, and, alas, there is no such animal.  Almost all of the papers of any merit are available either freely or for large sums of money on the Internet.  What if everything academic should be free?  A workaround occurred to me: Summarize the essentials of rare or paywalled papers.  I got an OK on this idea from the community, but I don’t have the time or the desire to carry it out.  I also can’t guess how the library evolved after I left.

The intellectual property of my sample is not lost, even if the ideas have, to some extent, lost their hold on the world: One of the chief products of Formel was the CAML language, which, alas, has been pushed out on the rankings by it’s closest rival, Haskell, which is, itself, at the bottom of the list.

My binders were organized into 5 topics:

  • Unification on first-order terms
  • Derivations of the unification algorithm
  • Knuth-Bendix critical-pair completion algorithm
  • Completion in equational systems and term rewriting systems
  • Complexity and expressibility of unification and completion

Here is what they contain (or contained, if I end up recycling them):

Unification on first-order terms

Derivations of the unification algorithm

Knuth-Bendix critical-pair completion algorithm

Completion in equational systems and term rewriting systems

  • Automatic proofs by induction in theories without constructors. 1989. Information and Computation. Jouannaud, Jean-Pierre. Kounalis, Emmanuel. https://www.sciencedirect.com/science/article/pii/089054018990062X
  • A general completion algorithm for equational term rewriting systems and its proof of correctness. 1983. CRIN. Kirchner, H. No PDF found online.
  • Reveur-3: the implementation of a general completion procedure parameterized by built-in theories and strategies. 1987. Science of Computer Programming. Kirchner, Helene. Kirchner, Claude. https://www.sciencedirect.com/science/article/pii/0167642387900049
  • An Overview of Completion Algorithms. 1985. EUROCAL ’85. Llopis de Trias, Regina. No PDF found online.
  • Canonical forms for residue classes of polynomial ideals and term rewriting systems. 1983. Submitted to JACM. Llopis de Trias, Regina. No PDF found online.
  • Complete Sets of Reductions for Some Equational Theories. 1981. JACM. Peterson, Gerald E.. Stickel, Mark E. PDF behind paywall.
  • On word problems in equational theories. 1987. INRIA. Rusinowitch, Michael. Hsiang, Jieh. https://hal.archives-ouvertes.fr/inria-00075875/document
  • Equations and rewrite rules. 1980. Stanford U CSD. Huet, Gerard. Oppen, Derek C.. http://citeseerx.ist.psu.edu/viewdoc/download?doi=
  • Completion of a Set of Rules Modulo a Set of Equations. 1986. SIAM J. Comp. Jouannaud, Jean-Pierre. Kirchner, Helene. PDF behind paywall.

Complexity and expressibility of unification and completion


Jury Duty


I was seated in a criminal jury panel in Charlotte, in a case of felony gun ownership to be proved by constructive possession.  The prosecutor asked me these questions:

Do I know any police officers? (Yes: I practiced Aikido with some in New York.  No: I didn’t socialize with them off the mat.)

What kind of law does my wife practice? (Matrimonial and litigation, in New York.  No, not in North Carolina, she is not in the bar.)

Have I ever been in this courthouse? (Yes, to pay a speeding ticket.)

Who gave me the ticket, state police or CMPD? (Neither, my local town police.)

Was I treated unfairly?  (No, I was going fast.)

How was the case disposed? (I hired a good lawyer and she pled it down to Improper Equipment.)

I asked one question: “Can you please repeat the definition of constructive possession?  Does that mean in the house or lent to another person under control of this person?” (Yes, like that.)

Two ladies next to me confessed to owning guns: An AR-15 and two pistols each.  One used to be military police. The other was a local town cop.  The former MP, who was covered in tattoos and was once kept in jail over a dispute over jewelry with her mother, and another woman who had a vacation coming up in a few days, and I were recused under peremptory challenge by the prosecutor.  (The woman with vacation was denied recusal for cause by the judge and then given it by the prosecutor.)

When you look up peremptory challenge, most discussion is about recusal due to race. In this case, the prosecutor was a black woman, the defendant was a black man, and I am white.  So I don’t consider race an issue.  The MP was recused clearly because of unpleasant experience with the court system.  Why was I recused?  According to this article, probably I was too verbal.

Here are a couple of funny videos on jury duty (note: I wasn’t trying to get out of jury duty; I was just being myself):

To ASIS with love


Mum’s the word, mate, I understand it’s a secret.

I won’t say anything about this elevator:


I won’t mention that with Windows 10 XBox game record feature on the browser (Windows key + G), it is easy to record the entire sequence.  (Mac users: I don’t know.)

The DVR allows us to capture and re-experience a wonderful demonstration of the British locative adverb hyuh (sorry I don’t have the software handy to stretch it out a little bit, you just have to savor it’s quick appearance at the end):

Don’t forget the clock:


People don’t usually interview at 1:45AM, so maybe it’s 1:45 PM!

Flying to Narita? That’s in Tokyo.

Regarding the attendant:


  1. She likes you to wait quietly while she dithers
  2. She wants you to note that it is busy today.  She doesn’t want you to ask if she’s worried because she will think you think she has behavioral health challenges..
  3. Tell her work will be over soon.
  4. Tell her you don’t want to bother her.
  5. She has a partner?  Interesting choice of words.  And she gave you the seat you were hoping for, without you even having to ask!  Please gift her a rainbow unicorn:


Regarding these guys:

2 people

If you got your Windows Game DVR on, you might spot Ben, Alicia, Darryl and Kate.  I didn’t see Paul or Lisa, maybe I missed them.

Spies generally don’t do this:


Finally, regarding these yentas (can they possibly all be the same woman?  did they hire triplets? or use some really good green screen compositor? was the casting budget a bit tight? or do all Australians look alike? ):


Carefully reviewing the recording will tell us the following 5 things:

  • There is a noodle shop around the corner from Emerald St.
  • One of these ladies likes fettuccine.
  • There are 6 courses on the fixed menu.
  • Joan stood them up
  • Australian software developers really like spinning cubes:


If you care about any of this, please feel free to apply for this job, using code 29ZZ9.  You’re welcome!

NF1 thoughts

I like to encourage scientists to pursue research in NF1.

NF1 is an area where there is a fair amount of GWAS work (see Wash U, Broad Institute).  NF1 arises due to mutations in the neurofibromin 1 gene.  The disease has a highly variable outcome depending on the mutation site.  Very little is known about genotype-phenotype correlation in NF1.

The NF1 gene was discovered and patented in 1993, but there hasn’t been significant progress towards a cure since then.   The current leader in NF1 research is the Children’s Tumor Foundation.  They focus on the traditional wet lab drug discovery pipeline.

Gene therapy is the most attractive solution, but the only person who has attempted work in this area is David Segal at UC Davis, whose 2014 Army-funded attempt failed. There is a correlation with NF1 gene mutations and autism.

NF1 is in the family of Rasopathies, so work in this area naturally leads into work on a much larger class of rare diseases that need attention.  Hence it is a rich and deep field, filled with scientific opportunity.

Bitcoin thoughts

I’m not interested in trading Bitcoin.  It’s too hard to time when the crash will come.  It’s important to keep in mind, it’s not Tulip bulbs.  There is a rational basis for the currency.  Unlike traditional currencies:

  1. Flows from one country to another are not tracked
  2. Sender and receiver of a flow are anonymous, unlike any bank transfer or credit card transaction
  3. Flows are not taxed
  4. Balances are not identified with any country or legal jurisdiction
  5. No central bank can expand or contract the money supply for political reasons

These are benefits for Gold bugs, tax dodgers, rebels and criminals.  All of the value resides there.  I expect the competitive response to this will be a universal currency, UN-style, using the same technology, but addressing some of the above needs in some kind of legal way.  When that happens, Bitcoin will drop to 0 except for purely criminal transactions and other transactions requiring secrecy.

불야성 White Nights and Inspector O


불야성, available on Netflix as White Nights, is a sort of corporate takeover procedural on one level, which is interesting for it’s catalog of uniquely Korean tax-dodging strategies and uniquely Korean takeover-related strong-arm tactics and stylized intimidation.  Read together with the Inspector O series of state security procedurals (which are written by an American, about North Korea), the two may bring us a little closer to an understanding of KJU and the Korean gestalt.  (Maybe that’s promising too much for a TV show and some spy novels.  But still.)

That the tactics on display over 20 episodes are aimless, confusing and baffling is not inconsistent or uninformative or inauthentic. They are what they are.  It’s handy to have them all in one place.  That they are also curiously dry and unengaging is also perhaps not inauthentic.  Who really cares what North Korea’s next provocation is on a day to day basis?  They want us to care.  We want to care.  But really, it’s hard to keep up that level of excitement all the time.  The Inspector O novels kind of speak to this as well.  They are quiet, aimless, without well-resolved conflicts or clear scenarios.  They go on.  They end.  One kind of leads into the next.  The character ages.  His nephew takes the spotlight.  One wonders how authentic they can be, written by a Westerner about a closed society.

Still, they are quite readable, and consistent with 불야성.

The other level and incentive for watching 불야성 is for the simmering w4w romance which is it’s spine.  Unlike the typical Korean drama love quadrangle, the romance in this show is carried on, completely in the closet, by the two female leads, with the closet kept well shut by a male lead who is platonically passed back and forth through the show by the two female leads.

The female chemistry has inspired some head-scratching examinations of this theme, and more than a few Youtube paeans.  Here are some of the best:



Computing the PDF of the sum of N moves of an empirical PDF for USDJPY 1-minute moves

[Cross posted.]

Per-minute tick data for USDJPY is available here. Suppose we download this file to usdjpy.txt and then save it into a Numpy array in Python 3 as follows:

import numpy as np
with open('USDJPY.txt','r') as f: data=f.readlines()
data=[x.split(',') for x in data][1:]
jpy=np.array([float(close) for (ticker,yy,time,open,high,low,close,vol) in data])

The per-minute returns in USDJPY, expressed in basis points, will be:


Define a histogram function and empirical PDF function as follows:

def histc(X,bins):
    map_to_bins = np.digitize(X,bins)
    r = np.zeros(bins.shape)
    for i in map_to_bins:
        r[i-1] += 1
    return [r,map_to_bins]

def epdf(S,numIntervals=100):
    if ncount[1]>len(S)/2:
    return (x,relativefreq)

The empirical PDF of USDJPY 1-minute pip returns is then:


which if we plot it

from bokeh.plotting import figure, show
from bokeh.io import output_notebook
simple=[(x[i],int(100*rf[i])) for i in range(rf.shape[0]) if int(100*rf[i]) > 0]
X=np.array([x for x,y in simple])
Y=np.array([y for x,y in simple])

Looks like this:

PDF of 1 minute move of USDJPY

Now suppose I want to know what could happen in an hour (60 one-minute moves). Following the answer to this question, I could convolve the EPDF above 60 times and I should get the right answer. I think this would look something like this:

def step_pdf(pdf1,pdf2):
    return pdf

from functools import reduce
pdf60=reduce(step_pdf,[rf for i in range(60)])

If I then plot the new pdf60 on top of the old pdf


I see (call this “Convolution PDF60”):

Convolution PDF60

The blue line is my 60-minute PDF from the above 60-fold convolution. It is smoother, which I expect, but it is still roughly in the same range as the original 1-minute PDF, which I do not expect. So now I will try a more constructive way of generating the 60-minute PDF: I will construct as many 60-minute samples randomly as I have 1-minute samples, by summing randomly selected vectors of size 60 from my original population of 1-minute moves. Then I will compute the empirical PDF of the result. I completely trust this construction, so I will use it as a benchmark against my original construction. So:

djpy60=np.array([djpy[draws[i]].sum() for i in range(n)])

Now if I plot pdf60:


I see a much wider distribution of 60-minute moves, which corresponds much more strongly to my intuition (call this “Monte Carlo PDF60”):

Monte Carlo PDF60

Question: Why aren’t my Convolution PDF60 and my Monte Carlo PDF60 in agreement?