Everything in Context

In Dale's Proof Search Foundations for Logic Programming talk, he gives a great minimalist example of an interactive system: toggling a switch. The encoding in Forum , a logic programming language based on full linear logic, goes like this: flip on off. flip off on. toggle G o- sw V * flip V U * (sw U -o G) or in logic, \[ \exists u,v.[sw\ v\otimes flip\ v\ u \otimes (sw\ u \multimap G)] \multimap toggle\ G \] (Yes, I mainly did that to test the $$\LaTeX$$ rendering script I'm using.) The talk I linked to gives a derivation (which I won't painstakingly copy here) illustrating the execution of the program: the goal sequent $$\Gamma; \Delta, sw\ on \longrightarrow toggle\ G$$ evolves through proof search into $$\Gamma; \Delta, sw\ off \longrightarrow G$$. But this is something of a counterintuitive, higher-order encoding. The "action" by a hypothetical user of toggling the switch must be indexed by $$G$$, the goal that continues the program. Her

As a teaser-trailer to the ideas I have been long overdue to write up, allow me to play some silly games with words. All claims herein are nontechnical and unsubstantiated. PL theorists are fond of the snowclone X-as-Y, "props-as-types" and "proofs-as-programs" being the pervasive example in functional programming. When we similarly try to explain logic programming logically , what comes out is more like "props as programs" and "proofs as traces ". Put another way, in functional progamming, computation is proof reduction while in logic programming, computation is proof search . So, then, what is a game? (I mean in the sense of "something humans play for fun," and specifically "as a piece of software", not the game-theory sense.*) At a rough gloss, a game is an interactive program. An execution of a game alternates computation and accepting human input. Interactive fiction is a minimal distillation of the idea (in that it

I implemented a version of the winnow algorithm for online learning in SML, because I was trying to understand learning algorithms in terms of coinductive data. The idea behind a learning algorithm, as I understand it (as someone who was just taught about them yesterday), is that given a stream of tagged inputs (like images marked with the locations of faces), you should get better and better at predicting the tags -- specifically, you should make a number of total mistakes bounded by the input size. Alternatively, you can think of the "tags" as a function from input to answer (for simplicity, from bitstring to bit) that the learning algorithm is trying to approximate. So the "learner" gets to take this function, which I call the "reference function", as an input, and compare its predictions to the actual result, which it can use to update some priors. Roughly, it has the shape: 1. Given an input, make a prediction 2. Check the answer with the ref

I recently finished LFinLF , a mechanized proof of the metatheory of LF, which took me about two and a half years and 36,503 lines of Twelf. I should focus my exposition efforts about it into a paper, but I thought I should update the occasional follower of this blog with the result. There are a few remaining questions I have been intrigued to consider as a result of finishing this proof: Can the common folklore that "we don't need family-level lambdas" be made formal? I used them in my proof to define translation: all LF terms translate to normal Canonical LF terms by way of eta-expansion; for families to be treated similarly, we need lambdas to expand the ones at pi kind. But there are other ways to do it which I think would shed varying degrees of light on why  we do without them. This proof formalizes the correctness of (a particular algorithm for) LF type checking ; could we also verify type reconstruction? Could I formalize the (also folkloric, though from sli

I recently tried to have a research conversation over Twitter -- always a questionable choice -- with an algorithms researcher, spurred by my comment that I was surprised to be able to find no work (at a cursory glance) on automatic deduction or checking of asymptotic runtime analysis.  After all, went my thought process, when a TA looks at the solutions to my Graduate Algorithms homework and determines that the pseudocode meets the runtime signature specified in the assignment, a certain amount of it is entirely mechanical.  In  Constructive Logic  at CMU, we use  Tutch  to give students automatic feedback on natural deduction proofs -- something that's very simple  to check by hand but which can be learned much more quickly with a rapid sequence of alternating attempts and feedback. The comment was met with skepticism, which I eventually decided to consider warranted at least to the extent that we want to a) perform analyses that require constructing adversarial input and b) in

I'll start out using this blog as a progress tracker, and maybe eventually I'll have the go to write some exposition that may be helpful to others. For now, expect self-indulgent omission of details! By way of introduction, though, I ought to explain some of what I'm currently doing so that future updates will have some context. My primary research project is formalizing the metatheory of LF in Twelf  (colloquially, "LFinLF," because LF is the underlying representation theory of Twelf).  What I am ultimately proving is decidability of typechecking for a dependent type theory; how  I am proving it is syntactically, without logical relations, via translation to syntactic canonical forms.  Chantal Keller presented  essentially the simply-typed case of what I am doing during one of the ICFP workshops this past fall, with two significant departures: for one, her canonical forms presentation was given in spine form (a more focussing-inspired syntactic separation whe