%{
__NOTOC__

In this lecture, Karl uses Prolog notation. I'm going to skip a step and go ahead and start using Twelf, since I've got all this infrastructure set up to incorporate pretty Twelf into web pages. For the purpose of this exercise, this only means that we have to declare types for things and that we write <tt>connect a b</tt> instead of <tt>connect(a,b)</tt>
for facts representing a connection from <tt>a</tt>
to <tt>b</tt>, and we say <tt>D <- A <- B <- C</tt> instead of <tt>D :- A, B, C</tt> for a three-premise rule.

You'll notice there's a box on the upper-right hand corner that calls this page "Literate Twelf." This is related to the idea of [http://www.literateprogramming.com/ Literate Programming] - this wiki page is itself a page of valid Twelf code.

If you'll forgive the ugly illustration, we're interesting in answering questions about rechability on this acyclic graph (we want it to be an acyclic graph!)

<code>
   -> b <-
  /       \   
 /         \ 
a---------->c----->d
</code>

}%

node : type.
a : node.
b : node.
c : node.
d : node.

connect : node -> node -> type.
reaches : node -> node -> type.

connect/a-b : connect a b.
connect/a-c : connect a c.
connect/c-b : connect c b.
connect/c-d : connect c d.

reach/refl  : {X: node} reaches X X.
reach/trans : {X: node} {Y: node} {Z: node} reaches Y Z -> connect X Y -> reaches X Z.

%{

'''NOTE:''' You don't have to write the &Pi; bound things, so you could have used:
<twelf name=dsfadsf>
reach/refl  : reaches X X.
reach/trans : reaches Y Z -> connect X Y -> reaches X Z.
</twelf>
(Twelf assumes you meant to &Pi;-bind capitalized things but were too lazy to write the &Pi;, so it does it for you.

I can ask the engine to ask questions about reachability, which will essentially perform a depth-first search on the graph.

I can confirm that there is one way through the graph from <tt>a</tt> to 
<tt>d</tt> (the notation <tt>%query 1 *</tt> isn't important for you to remember, but it means that I want one answer
no matter how many times I try)

|check=decl}% 

%query 1 * reaches a d. 

%{

...I can ask the engine to verify that there are no paths through the graph from <tt>b</tt> to <tt>a</tt>:

|check=decl}%

%query 0 * reaches b a.

%{ 

...finally, I can use a capital letter (metavariable or substitution variable) <tt>Z</tt> to ask, what is EVERY path, starting from
<tt>a</tt>, in the graph? Turns out there are 5 (<tt>b</tt> can be reached in two different ways):

|check=decl}%

%query 5 * reaches a Z.

%.

= The LF Logical Framework =

== Syntax ==

<math>
K ::= \texttt{type} \mid A \rightarrow K
</math>

<math>
A ::= \Pi x{:}A.A \mid \lambda x{:}A.A \mid A~M \mid \texttt{a}
</math>

<math>
M ::= x \mid \lambda x{:}A.M \mid M~M \mid \texttt{c}
</math>

== Typing Rules ==

=== Kinds ===

Kinds ''K'' classify types ''A''.

<br/>

<math>
{}
\over
{\texttt{type} : \texttt{kind}}
</math>

<br/>

<math>
{A : \texttt{type} \qquad
K : \texttt{kind}}
\over
{A \rightarrow K : \texttt{kind}}
</math>

=== Types ===

Types ''A'' classify terms ''M'' and are classified by kinds ''K''.

<br/>

<math>
{A : \texttt{type}\qquad
x : A \vdash B : \texttt{type}}
\over
{\Pi x{:}A.B : \texttt{type}}
</math>

<br/>

<math>
{A : \texttt{type} \qquad
x : A \vdash B : K}
\over
{\lambda x{:}A.B : A \rightarrow K}
</math>

<br/>

<math>
{A : A' \rightarrow K \qquad
M : A'}
\over
{A~M : K}
</math>

<br/>

<math>
{\texttt{a} : K \in \Sigma}
\over
{\texttt{a} : K}
</math>

=== Terms ===

Terms ''M'' are classified by types ''A''.

<math>
{A : \texttt{type} \qquad
x : A \vdash M : A'}
\over
{\lambda x{:}A . M : \Pi x {:} A . A'}
</math>

<br/>

<math>
{M_1 : \Pi x{:}A . A' \qquad
M_2 : A}
\over
{M_1~M_2 : A'[M_2/x]}
</math>

<br/>

<math>
{\texttt{c} : A \in \Sigma}
\over
{\texttt{c} : A}
</math>