robsimmons

structure Edge:> sig

   (* Asserts some number of less-than relationships between identifiers *)
   val addRelationships: (string * string) list -> unit

   (* Returns true if two identifiers are related *)
   val related: string * string -> bool

end = struct
   open Symbol

robsimmons

I think some of the commenters were confused by the notation $\Gamma \vdash A \downarrow B$, which I have only seen written as $\Gamma [ A ] \vdash B$ or $\Gamma \vdash A > B$. The downarrow comes, as you note in a comment, from Andreoli's notation, but that notation is more common in presentations of sequent calculi for classical logics, at least in my experience. The notation I'll use is the one with $>$ instead of $\downarrow$, which comes from Cervesato and Pfenning's "A Linear Spine Calculus."

Two proof systems
-----------------

So, to restate the goal, we have the following sequent calculus for first-order, minimal logic:

$$
{P \in \Gamma \over \Gamma \Rightarrow P}{\it init}
\qquad

robsimmons

/* 
   Some simple Github-like styles, with syntax highlighting CSS via Pygments.
*/
body{
	font-family: helvetica, arial, freesans, clean, sans-serif;
	color: #333;
	background-color: #fff;
	border: none;
	line-height: 1.5;
	margin: 2em 3em;

robsimmons

/* 
   Some simple Github-like styles, with syntax highlighting CSS via Pygments.
*/
body{
	font-family: helvetica, arial, freesans, clean, sans-serif;
	color: #333;
	background-color: #fff;
	border: none;
	line-height: 1.5;
	margin: 2em 3em;

robsimmons

- val {get, poll} = Conductor.package "/tmp/smackage" "rob-toy";
val get = fn : SemVer.semver -> unit
val poll = fn : unit -> (string * SemVer.semver) list
- poll ();
val it =
  [("02d584bf0b14704e98efc324efe6d05fb31ce4af",(0,0,1,NONE)),
   ("23597de0addda54e21d89b70f6c70ae2da75d7b8",(0,1,0,NONE)),
   ("139359d7589ca69aebfada148d8d4ad191bdeb74",(1,0,0,NONE)),
   ("0669dd7562bad0f580a0016d7b5ac88af9182512",(1,1,0,NONE)),
   ("bea772c3886a881a7a02023c89e05881a7a7ce3f",(1,1,1,NONE)),

robsimmons

datatype foo = A | B | C | D
(*[ datasort ab = A | B ]*)
(*[ datasort bc = B | C ]*)
(*[ datasort abc = A | B | C ]*)

(* This works *)
(*[ val x: ab & bc ]*)
val x = B

(* This, however, does not...

robsimmons

structure A = 
struct
   val say = fn () => print "A\n" 
end

structure B = 
struct
   val say = fn () => print "B\n"
end

robsimmons

\documentclass[12pt,openany]{article}

\begin{document}

\setcounter{page}{51}

Basically just read \cite{And01}.

\begin{thebibliography}{WCPW02}

robsimmons

Original puzzle: https://twitter.com/tausbn/status/251686364788170752

First observation: 

If G ->* {0} implies G =>* {0}, it must be the case that if 
G -> G' and G' =>* {0} then G =>* {0}.

Proof: Given G -> G' and G' =>* {0}, we have G' ->* {0}
immediately (->* contains =>*) and G ->* {0} by direct
composition (G -> G' ->* {0}). Then we have G =>* {0} by the

robsimmons

CREATE TABLE `feedback` (
   `job` int NOT NULL,
   `task` char(20) NOT NULL,
   `payload` longtext NOT NULL,
   `timestamp` timestamp NOT NULL DEFAULT CURRENT_TIMESTAMP,
   UNIQUE KEY `job` (`job`, `task`),
   CONSTRAINT `feedback_job` FOREIGN KEY (`job`) REFERENCES `job` (`job`) ON DELETE CASCADE
);