Skip to main content

Intro

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 wherein applications consist of a head and a list of arguments that make it fully-applied), and for two, her formalization was in Agda, making the proof methodology quite a bit different (in terms of representing contexts and hypotheticals).

You can think of this proof as having three parts:

1)  Metatheory for the canonical forms language. Because standard substitution (of the sort LF would give us for free) doesn't preserve canonical forms, we judgmentally define hereditary substitution, which means actually proving a substitution theorem.  I finished this my first year in grad school.

2)  Completeness of the translation into canonical forms.  Definitionally equivalent things in LF should translate to syntactically identical canonical forms, and analogous judgments should hold of each. I finished this my second year.

3)  Soundness of the translation into canonical forms: if two LF terms translate to the same canonical form, then they are definitionally equivalent.  This amounts to defining a back-translation -- really just a transliteration -- from canonical forms to LF, and proving that a term will always round-trip (translate, then transliterate) to an equivalent term. This is the proof that has been holding me up for about a year, but we had a breakthrough last month which I hope to post about soon.

Apart from that, I've also been thinking a bit about logic programming with mechanisms for linearity plus contingent reasoning, so a post about that should go on the queue as well.

Comments

Popular posts from this blog

Using Twine for Games Research (Part II)

This preliminary discussion introduced my thoughts on using Twine as a tool for creating prototypes for games research. I'll start with documenting my first case study: a hack-and-slash RPG-like setting where the player character has a record of attributes ("stats") that evolve through actions that turn certain resources (money, health, items) into others. I've selected this hack-and-slash example because it falls outside the canonical "branching story" domain thought to be Twine's primary use case, but it is not too much trickier to implement. It relies crucially on the management of state in ways that simple branching stories would not, but it does so in a fairly straightforward way.

If all goes well, this post may also serve as a tutorial on the "basics" of Twine (links + variables + expressions). In particular, I'll be using Twine 2/Harlowe, and I haven't seen many tutorials for this new version published yet.

To me, the main "…

Using Twine for Games Research (Part III)

Where we last left off, I described Twine's basic capabilities and illustrated how to use them in Twine 2 by way of a tiny hack-and-slash RPG mechanic. You can play the result, and you should also be able to download that HTML file and use Twine 2's "import file" mechanism to load the editable source code/passage layout.

Notice that, in terms of game design, it's not much more sophisticated than a slot machine: the only interesting decision we've incorporated is for the player to determine when to stop pushing her luck with repeated adventures and go home with the current spoils.

What makes this type of RPG strategy more interesting to me is the sorts of decisions that can have longer-term effects, the ones where you spend an accumulation of resources on one of several things that might have a substantial payoff down the road. In a more character-based setting, this could be something like increasing skill levels or adding personality traits.

Often, the game-…

Why I don't like the term "AI"

Content note: I replicate some ableist language in this post for the sake of calling it out as ableist.

In games research, some people take pains to distinguish artificial intelligence from computational intelligence (Wikipedia summary), with the primary issue being that AI cares more about replicating human behavior, while CI is "human-behavior-inspired" approaches to solving concrete problems. I don't strongly identify with one of these sub-areas more than the other; the extent to which I hold an opinion is mainly that I find the distinction a bit silly, given that the practical effects seem mainly to be that there are two conferences (CIG and AIIDE) that attract the same people, and a journal (TCIAIG - Transactions on Computational Intelligence and Artificial Intelligence in Games) that seems to resolve the problem by replacing instances of "AI" with "CI/AI."

I have a vague, un-citeable memory of hearing another argument from people who dislike the…