The trek goes on

The immediate sublist induction problem seems to point towards some general theory about datatype and program integration.

Parametricity is used to prove that the types of both the standard induction principle for natural numbers and the immediate sub-list induction principle are uniquely inhabited (up to extensional equality).

I chaired the APLAS 2023 student research competition and the associated poster session, and here’s a report, which may be useful to future SRC chairs.

A derivation from a generic top-down specification of divide-and-conquer computation to a bottom-up implementation is reformulated and clarified using dependent types, category theory, and string diagrams.

Some rough notes about amplitude amplification and Jordan’s lemma, with some extrapolations about what we should have in a high-level quantum-algorithmic language from what I’ve seen.

If the result of a measurement is a uniform distribution, then no quantum information is lost. It turns out that this intuition can be straightforwardly formulated in the graphical quantum theory.

To complete the Bell basis trilogy, we also look at entanglement swapping, which, though slightly more complex, can be presented naturally in ZX-calculus.

Another popular example that makes use of the Bell basis is dense coding, which is a name I find misleading though.

Two graphical presentations of quantum teleportation are given, one directly working with concrete definitions in ZX-calculus, and the other developing a higher-level structure.

The Bernstein-Vazirani algorithm is closely related to Deutsch–Jozsa, but I have to fall back to the conventional understanding of the oracle construction —encoding function outputs as phases— to deal with this one.

The Deutsch–Jozsa algorithm is one of the simplest quantum algorithms, although the traditional presentation is still rather obscure (at least to beginners). With the help of the ZX-calculus, we can actually see that the algorithm is no more than a twisted form of a simple computation.

A rudimentary experiment in writing imperative programs functionally.

If we model computation as generating a potentially infinite colist of states, then termination is the ability to cast this colist into a finite list.

We take a look at the left scan as a simple application of the traced state monad, which gives us an opportunity to revisit productivity checking and Danielsson’s embedded language technique.

The traced state monad is useful for revealing intermediate states even when computation does not terminate and reach a final result. Reasoning about the traced state monad is elementary but inherently extensional, which used to be a problem for proof assistants, but Cubical Agda changes all that.

I played a bit with (a simplified version of) Allais et al’s traversal operator for syntax trees with λ-style binders and variables as de Bruijn indices — which translates terms to functions taking an environment as input and manages the environment for the user — and experimented with a corresponding induction operator (not really successfully).

This year more people started to join me for tea, and I decided to set up a ‘tea bar’ with which I can hold a nice ‘tea party’ in my office anytime I like.

A bit of fun with identifying states on the Bloch sphere in ZX-calculus, which involves a bit of fun with trigonometry.

We perform a (not so successful) experiment that proves a simple graph-theoretic property (an induced sub-graph of a directed acyclic graph is also acyclic) in relational calculus.

A (simple) construction that realises the principle of deferred measurement is described (and proved correct) in ZX-calculus.

Naturality enters the picture as we prove that the two formulations of optimising definitions in terms of universality and isomorphism are equivalent.

An important special case of adjunctions is Galois connections, which can be very helpful for reasoning about order-theoretic optimising definitions.

The universal property of (categorical) products can be reformulated as a useful family of isomorphisms.

Quantum theory starts with a few postulates about the states of quantum systems and how they evolve, and there are two formulations, one in terms of unit vectors and the other in terms of density operators. This post shows that the unit vector formulation gives rise to a very simple transition system, which we can then transform and optimise to get a transition system corresponding to the density operator formulation.

We experiment with formulating the paradoxical arguments for the undecidability of the halting problem and, more generally, Rice’s theorem in a modally typed setting using (a variation of) Kavvos’s intensional recursion, whose type corresponds to the Gödel–Löb axiom.

With path calculations similar to those in 0011, we can prove a couple more important theorems in HoTT: Hedberg’s theorem and the incompatibility between univalence and the unconstrained law of excluded middle.

From one lemma, this post proves in Homotopy Type Theory that (i) equality types on a contractible type are also contractible, and that (ii) the definitions of sets and mere propositions match the general definitions of 0-types and (−1)-types.

At FLOLAC ’20 I will present Conor McBride’s showcase example in his original ornament paper, where the evaluation of additive expressions (which he calls ‘Hutton’s razor’) is compiled to instructions for a stack machine, and the preservation of semantics is proved purely by datatype indexing.

As a short intern project, we’re formalising a semantics-preserving translation from finitely typed circuits to boolean ones, so that properties proved for the compiled boolean circuits by SAT solving can be transferred back to the typed circuits.

One nice thing that happened over the past few months was getting all the facilities I want in my office, of which this post is a quick tour. Quite a few pictures are included.

A while ago I wrote 0004 about eliminating quantifier alternation, which took a fair amount of logic formula manipulation. Not long after that, my colleague Yun-Sheng Chang came up with a reformulation that makes the solution much more streamlined; this post contains my presentation of the reformulation, along with a higher-level recap of what I did in 0004.

程式語言學對符號有近乎偏執的愛好與要求：我們以符號為工具精準簡練地表達程式與相關概念，用符號做厲害的事（證明程式性質），設計易用的符號，並且特別喜歡有多重內涵 — 特別是具有數學和邏輯學意義 — 的符號。本文為科普向。

This post is an incomplete digest of Andrej Bauer’s note What is algebraic about algebraic effects and handlers?. My goal is to arrive at a reasonable definition of handlers. (Spoiler: I don’t manage to achieve that goal, although we will see Bauer’s definition.)

I found that the type theory people and the verification people think about the same logical formulas in different or even opposite ways, which is quite interesting. This post contains a summary of an abstracted (and in fact distorted) version of the problem we discussed, and records some of the different ways of thinking of the two camps.

The key is to use the contrapositive universal property of the floor function.

Recently I reread Nils Anders Danielsson’s POPL 2008 paper Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures, whose technique (implemented in Agda) has been adopted by a few groups of people…

If we regard the big-O notation as denoting classes/sets of functions, which I call ‘order classes’, we can start talking about their structures, and one such structure is the semiring of order classes. …

I am informally notified today that my application for the position of assistant research fellow at the Institute of Information Science, Academia Sinica (the national academy of Taiwan) has been approved, and I can expect to start at the beginning of the next year. With the start of the new job, it looks like a good opportunity to pick up the habit of blogging again. …