dylnb/index.html

## index.html
<html>
  <head>
    <title>Lambda Calculator - Exercise File Format</title>
    <meta charset="UTF-8" />
    <style>
      pre {
        border: 1px solid #CCCCCC;
        background-color: #EEEEEE;
        padding: .5em;
      }
      th { padding-left: .75em; padding-right: .75em }
      li { margin-bottom: .5em }
    </style>
  </head>
  <body>

    <h1>Lambda Calculator - Exercise File Format</h1>

    <p>Exercise files created by the instructor are saved as plain-text files, usually with a <tt>.txt</tt> file extension. You can edit this files with, for instance, the Notepad program on Windows. When using Microsoft Word or another office suite, be sure to save the file as a Text Only-formatted file. When using special or international (non-ASCII) characters, files should be saved in the UTF-8 Unicode character encoding.</p>

    <p>An example exercise file is given below.</p>

    <pre>
# Lines that begin with a hash are ignored.

Homework 1

constants of type e : a b-c
constants of type &lt;e,t&gt; : P-Q
variables of type e : x-z
variables of type &lt;et&gt; : X Y

exercise semantic types
points per exercise 10
title Semantic Types
directions Give the semantic type of the following lambda-expressions.

c
P(c)
Q(x) V ~Q(x)
Lx[P(x) &amp; Q(x)]

exercise lambda conversion
points per exercise 15
title Lambda Conversion
directions After checking that the type of the function and the type of the
directions argument(s) match, simplify the following expressions performing
directions one lambda-conversion at a time.

Lx[P(x) &amp; Q(x)] (a)
LxLy[R(a,y) &amp; Q(x)] (a) (b)
Lx[a] (b)
LxLx[P(x) -> R(x,c)] (a) (b)
</pre>

      <h2>File Format Basics</h2>

      <p>Blank lines in execise files are ignored, and lines that begin with a hash (#) are also ignored. You can use hashes to store notes in the file that won't be read by the Lambda program, but of course keep in mind that students can view such notes if they open the exercise file in a text editor themselves.</p>

      <p>The first (non-ignored) line of every exercise file is the title of the exercise to be shown to the student, and for the instructor's use later when reviewing the students' work. In the example above, this is <tt>Homework 1</tt>.</p>

      <p>Following this line, a line is either a <i>directive</i> to the Lambda program, or it is an <i>exercise</i>.</p>

      <h2>Directives</h2>

      <p>Directives are lines that begin with specially recognized commands. These are explained below.</p>

      <dl>

        <dt><tt>constants of type ___ : ___</tt></dt>
        <dt><tt>variables of type ___ : ___</tt></dt>
        <dd>
          <p>These directives specify the typing convention for variables and constants found in the exercises. If none of these directives are present in an exercise file, the default type assignments shown below are used. The first time this directive is used in an exercise file, the defaults are cleared, and the new type assignments apply for all exercises following the directive.</p>
          <p>A type can be either:</p>
          <p>an atomic type, which can be any single letter,</p>
          <p>a complex (function) type specified as &lt;T<sub>1</sub>,T<sub>2</sub>&gt;, for types T<sub><i>i</i></sub>, or</p>
          <p>a cartesian-product type, specified as T<sub>1</sub>*T<sub>2</sub>*T<sub>3</sub>....</p>
          <p>One-place predicates are typed as complex types. Two-place (or more) predicates are typed as functions from a cartesian-product type to another type, i.e. as <tt>&lt;T<sub>1</sub>*T<sub>2</sub>*T<sub>3</sub>,T<sub>4</sub></tt>&gt;. Commas may be omitted from complex types when the types on either side are both atomic.</p>
          <p>Examples:</p>
          <pre>
constants of type e : a b-c
constants of type &lt;e,t&gt; : P-Q
constants of type &lt;e*e,t&gt; : R S T
variables of type e : x-z
variables of type &lt;et&gt; : X Y
</pre>
  <p>These directives will always override previous uses of the directives, so you can change the typing conventions throughout the exercise file by issuing this directive again.</p>
  <p>The default typing conventions are:</p>
  <pre>
constants of type e : a-e
constants of type &lt;e,t&gt; : P-Q
constants of type &lt;e*e,t&gt; : R-S
variables of type e : u-z
variables of type &lt;et&gt; : U-Z
</pre>
  </dd>

  <dt><tt>points per exercise ___</tt><dt>
  <dd><p>This directive specified a numeric point value assigned to each exercise that follows the directive, or just until another <tt>points per exercise ___</tt> directive is found. The points value can be any rational number. It is up to the instructor to ensure that the total points add up to 100 if that is desired. Example:</p>
    <pre>points per exercise 15</pre></dd>

  <dt><tt>exercise ___</tt></dt>
  <dd><p>This directive begins a group of exercises and specifies the type of exercise in the group. The exercise type must be either <tt>semantic types</tt>, <tt>lambda conversion</tt>, or <tt>tree</tt>. These exercises are described below. The <tt>exercise ___</tt> directive <i>must</i> be followed by <tt>title ___</tt> and <tt>directions ___</tt> directives before any exercises are entered. Examples:</p><pre>exercise lambda conversion
exercise semantic types
exercise tree</pre></dd>

  <dt><tt>title ___</tt></dt>
  <dd><p>Specifies the title for the group of exercises. This directive must be specified after an <tt>exercise ___</tt> directive and before the actual exercises. Example:</p><pre>title Lambda Conversion</pre></dd>

  <dt><tt>directions ___</tt></dt>
  <dd><p>Specifies the directions to provide to the student for a group of exercises. This directive must be specified after an <tt>exercise ___</tt> directive and before the actual exercises. Directions can be split across multiple lines by repeating the <tt>directions ___</tt> directive. Example:</p>
    <pre>directions After checking that the type of the function and the type of the
directions argument(s) match, simplify the following expressions performing
directions one lambda-conversion at a time.</pre>
  <p>You can include predicate logic expressions inside the directions. By writing the expressions according to the directions below, and surrounding them in curly braces, they will appear to the student rendered nicely with the appropriate symbols for lambdas, etc.</p>
  <pre>directions The expression {Lx.Iy[P(y,x)]} has type &lt;e,e&gt;.</pre>
  <p>Greek letters may be included in two ways. 1) By preceding the name of the letter
    with a backslash, as in LaTeX. For instance, \alpha for lowercase alpha or \Omega for a capital omega. (Not all Greek letters are supported.)
    <!-- note something similar below within expressions and brackted trees -->
    2) By putting the special character directly within the text file (i.e. with
    Word's Insert Symbol), and saving the file in UTF-8 Unicode encoding.</p>
  <p>You can start a new paragraph in the directions by ending a line with
    two backslashes (\\), as in LaTeX.</p>
  </dd>

  <dt><tt>instructions ___</tt></dt>
  <dd><p>Specifies instructions for the following exercise only. This directive must be specified immediately before the exercise to which it applies. Instructions can be split across multiple lines and can include expressions in the same way as with the <tt>directions</tt> directive, described above. Example:</p>
    <pre>instructions This exercise is a trick question!
Lx[a] (b)</pre></dd>

  <dt><tt>multiple letter identifiers</tt></dt>
  <dt><tt>single letter identifiers</tt></dt>
  <dd><p>After this directive, identifiers can be either be words of more than
    one letter, or may only be single letters. When the <tt>single letter identifiers</tt>
    directive is set, certain abbreviations are accepted when reading predicate
    logic expressions. For instance, "Pabc" may be used to abbreviate P(a,b,c).
    When <tt>multiple letter identifiers</tt>
    is used, "Pabc" is treated as a single identifier. If neither directive is
    specified, <tt>single letter identifiers</tt> is assumed.</p></dd>

  <dt><tt>define ___ : ___</tt></dt>
  <dd><p>Defines lexical entries for use in tree exercises provided to the student. The student will be able to enter other lexical entries as needed. Multiple words can be given the same lexical entry by separating the words with comma. A word may be given multiple lexical entries by repeating the <tt>define</tt> line multiple times. A single lexicon is used for all exercises in the file. Example:</p>
    <pre>define Sue : s
define introduce, introduces : LxLyLz[introduces(z,x,y)]</pre></dd>

  <dt><tt>use rule ___</tt></dt>
  <dd><p>Indicates which composition rules are allowed to be used in tree exercises, including function application, non-branching nodes (copying the denotation of the single child node to the parent node), predicate modification, and lambda abstraction, based on the Heim &amp; Kratzer textbook. Example:</p>
    <pre>use rule function application
use rule non-branching nodes
use rule predicate modification
use rule lambda abstraction</pre></dd>


      </dl>

      <h2>Exercises</h2>

      <p>Lines that are not recognized as directives are assumed to be exercises, of the type specified in a preceding <tt>exercise ___</tt> directive.</p>

      <h3>Semantic Types Exercises</h3>

      <p>For this exercise type, the instructor enters an expression in predicate logic. The student's task is to provide the semantic type of the expression. For example, if the exercise is:</p>

      <pre>λx[P(x) ∧ Q(x)]</pre>

      <p>The student is expected to answer:</p>

      <pre>&lt;e,t&gt;</pre>

      <p>Or in an equivalent way, such as abbreviated as <tt>et</tt>.</p>

      <p>Predicate logic expressions can be entered in exercise files without needing to insert special characters like lambdas and wedges. This is described in more detail below. For the example above, the instructor enters into the exercise file:</p>

      <pre>Lx[P(x) &amp; Q(x)]</pre>

      <p>The correct answer, i.e. the type of this expression, does not need to be entered into the exercise file. The Lambda program will compute the correct answer itself.</p>

      <h3>Lambda Conversion Exercises</h3>

      <p>For this exercise type, the instructor enters an expression in predicate logic. The student's task is to simplify the expression by performing lambda conversions, one at a time. For example, if the exercise is:</p>

      <pre>λx.λy[R(a,y) ∧ Q(x)] (a) (b)</pre>

      <p>The student is expected first to answer:</p>

      <pre>λy[R(a,y) ∧ Q(a)] (b)</pre>

      <p>The Lambda program will check this intermediate answer and then allow the student to proceed to the next step:</p>

      <pre>R(a,b) ∧ Q(a)</pre>

      <p>It is possible to lambda-convert over higher types. This proceeds as follows:</p>

      <pre>
λX[X(b)] (λx. R(a,x))
(λx[R(a,x)]) (b)
R(a,b)
</pre>

      <p>In addition, non-reducible predicate logic expressions may also be provided in the exercise file, such as the expression <tt>P(x)</tt>. In this case, the student is expected to respond with the same expression.</p>

      <p>Sometimes creating an alphabetical variant is needed before proceeding to lambda conversion. In these cases, the Lambda program will realize that an alphabetical variant is necessary, and it will require that the student enters it before preceeding with simplification. An example of this is shown below:</p>

      <pre>
Exercise: λx.∃y[R(y,x)] (y)
Student's responses:
1) λx.∃yʹ[R(yʹ,x)] (y)
2) ∃yʹ[R(yʹ,y)]
</pre>

      <p>The correct answers to lambda conversion exercises, i.e. the simplifications of the expressions, do not need to be entered into the exercise file. The Lambda program will compute the correct answer (including the steps needed to reach it) itself.</p>

      <h3>How to enter predicate logic expressions</h3>

      <p>The Lambda program will read predicate logic expressions from exercise files. Predicate logic expressions may include:</p>

      <ul>
        <li>Constants and variables. Constants and variables must be single letters only, unless the <tt>multiple letter identifiers</tt> directive is used. Primes can be entered with the apostrophe. Some capital letters (A, E, I, and L) are treated specially by the Lambda program; see the note below on using these letters within constants and variables.</li>
        <li>Constants and variable with explicit types using an underscore to separate the name and the type, such as: x_e, X_&lt;e,t&gt;, etc. Composite types such as &lt;e,t&gt; must be written with brackets and cannot be abbreviated as "et". Explicit types are unnecessary when the typing conventions specified in the exercise file already provide a type for the identifier.</li>
        <li>Predicates, entered as P(a) or P(a,b,c) (or if the <tt>multiple letter identifiers</tt> has not been specified, in abbreviated form such as Pabc).</li>
        <li>The logical connectives, which can be entered according to the table below:
          <table>
            <tr><th>Connective</th> <th>You Type</th></tr>
            <tr><td style="text-align: center">¬</td><td style="text-align: center">~</td></tr>
            <tr><td style="text-align: center">=</td><td style="text-align: center">=</td></tr>
            <tr><td style="text-align: center">≠</td><td style="text-align: center">!=</td></tr>
            <tr><td style="text-align: center">∧</td><td style="text-align: center">&amp;</td></tr>
            <tr><td style="text-align: center">∨</td><td style="text-align: center">V</td> <td>(capital letter v)</td></tr>
            <tr><td style="text-align: center">→</td><td style="text-align: center">-&gt;</td></tr>
            <tr><td style="text-align: center">↔</td><td style="text-align: center">&lt;-&gt;</td></tr>
          </table>
          Operator precedence is as given in the table, except that the pairs →/↔, ∧/∨, and =/≠ represent operators at the same operator precedence, so expressions like (a = b ≠ c) is not well formed.</li>
        <li>Parenthesized expressions, using parens (...) or brackets [...].</li>
        <li>Quantifiers and binders, which can be entered using capital Roman letters according to the table below:
          <table>
            <tr><th>Quantifier</th> <th>You Type</th></tr>
            <tr><td style="text-align: center">∃</td><td style="text-align: center">E</td></tr>
            <tr><td style="text-align: center">∀</td><td style="text-align: center">A</td></tr>
            <tr><td style="text-align: center">λ</td><td style="text-align: center">L</td></tr>
            <tr><td style="text-align: center">ι</td><td style="text-align: center">I</td></tr>
          </table>
          For example, Ax[P(x)], AxEy[P(x) &amp; Q(y)], Lx[P(x)], LxLy.P(x,y) &amp; Q(y), Iz[king(z)]. Periods may separate multiple consecutive quantifiers/binders. After quantifiers and binders, a bracketed expression should follow to avoid scope ambiguity.</li>
        <li>To use capital E, A, L, I, and V as those letters in a constant or variable, precede the letter with a backslash (\) to indicate to the program to treat the letter following like normal, e.g. H\APPY, \L\ITT\L\E.</li>
        <li>Function application, which is an expression followed by another expression (usually in parenthesis and separated by a space), such as Lx[P(x)] (b).</li>
        <li>Single Greek letters may be used as constants or variables by preceding the name of the letter
          with a backslash, as in LaTeX. For instance, \alpha for lowercase alpha or \Omega for a capital omega. (Not all Greek letters are supported.)
          <!-- note use of Greek letters in directions and in bracketed trees --></li>
        <li>Numeric connectives, which can be entered according to the table below:
          <table>
            <tr><th>Connective</th> <th>You Type</th></tr>
            <tr><td style="text-align: center">⋅</td><td style="text-align: center">*</td> <td>(multiplication)</td></tr>
            <tr><td style="text-align: center">&lt;</td><td style="text-align: center">&lt;</td> <td></td></tr>
            <tr><td style="text-align: center">≤</td><td style="text-align: center">&lt;=</td> <td></td></tr>
            <tr><td style="text-align: center">&gt;</td><td style="text-align: center">&gt;</td> <td></td></tr>
            <tr><td style="text-align: center">≥</td><td style="text-align: center">&gt;=</td> <td></td></tr>
          </table>
          <li>Numbers can be entered and are treated as constants of type i.
            <li>Sets, set connectives, and set operators, which can be entered according to the table below:
              <table style="margin-bottom: 1em">
                <tr><th>Set Expression</th> <th>You Type</th></tr>
                <tr><td style="text-align: center">{ a, b, c, ... }</td><td style="text-align: center">curley braces and commas</td></tr>
                <tr><td style="text-align: center">{ x | P(x) }</td><td style="text-align: center">curley braces and the pipe | key</td></tr>
                <tr><td style="text-align: center">∅</td><td style="text-align: center">\emptyset</td></tr>
              </table>
              <table>
                <tr><th>Operator</th> <th>You Type</th></tr>
                <tr><td style="text-align: center">| ... |</td><td style="text-align: center">the pipe | key</td> <td>(set cardinality)</td></tr>
                <tr><td style="text-align: center">∩</td><td style="text-align: center">^^</td> <td>(two carrets)</td></tr>
                <tr><td style="text-align: center">∪</td><td style="text-align: center">VV</td> <td>(two capital V's)</td></tr>
                <tr><td style="text-align: center">⊆</td><td style="text-align: center">&lt;&lt;</td> <td></td></tr>
                <tr><td style="text-align: center">⊈</td><td style="text-align: center">!&lt;&lt;</td> <td></td></tr>
                <tr><td style="text-align: center">⊊</td><td style="text-align: center">&lt;&lt;&lt;</td> <td></td></tr>
                <tr><td style="text-align: center">⊇</td><td style="text-align: center">&gt;&gt;</td> <td></td></tr>
                <tr><td style="text-align: center">⊉</td><td style="text-align: center">!&gt;&gt;</td> <td></td></tr>
                <tr><td style="text-align: center">⊋</td><td style="text-align: center">&gt;&gt;&gt;</td> <td></td></tr>
              </table>
              <p>The intersection and union connectives bind more tightly than the other set and logical connectives.</p>
              <p>Note that the set notation { x | P(x) } is a binder. All variables to the left of the vertical bar (which is usually just a single variable) bind occurrences of that variable to the right of the bar.</p></li>
      </ul>

      <h3>Tree Exercises</h3>

      <p>In tree exercises, the instructor provides a tree in labeled brackets notation. The student is presented with a graphical rendition of the tree and is expected to provide the denotations of the terminal nodes and to evaluate the denotations of the nonterminal nodes up to the root.</p>

      <p>To create a tree exercise, simply provide the brackets notation of the tree. To give nonterminal node labels, precede the label with a period. Nodes are not required to be labeled.</p>

      <pre>[.S [.NP John] [.VP [.V' loves] Mary] ]

[ [the [fast man]] [ate [many apples]]]</pre>

      <p>Superscripts and subscripts may be indicated with the caret (^) and underscore (_). Only integer subscript indices are allowed. On nonterminals, these play no special role in the program. They are for pretty display purposes only.</p>

      <pre>[.DP_1 the [.NP_1 man [that_1 [I [ [.V^0 saw] t_1] ] ] ]]</pre>

      <p>Traces and pronouns with indices (t_<i>i</i>, he_<i>i</i>, she_<i>i</i>, it_<i>i</i>, him_<i>i</i>, her_<i>i</i>, himself_<i>i</i>, herself_<i>i</i>, itself_<i>i</i>, his_<i>i</i>, hers_<i>i</i>, its_<i>i</i>, theirs_<i>i</i>) are automatically given the denotation of g(1), g(2), etc. according to the index.</p>

      <p>Relative pronouns with indices (that_<i>i</i>, what_<i>i</i>, which_<i>i</i>, who_<i>i</i>, such_<i>i</i>) and bare indices (1, 2, 3, ...) are treated as "bare index" terminal nodes for lambda abstraction, following Heim &amp; Kratzer.</p>

      <p>Single Greek letters may be used as terminal and nonterminal labels by preceding the name of the letter
        with a backslash, as in LaTeX. For instance, \alpha for lowercase alpha or \Omega for a capital omega. (Not all Greek letters are supported.)
        <!-- note use of Greek letters in directions and expressions--></li>

</body>
</html>
	<html>
	<head>
	<title>Lambda Calculator - Exercise File Format</title>
	<meta charset="UTF-8" />
	<style>
	pre {
	border: 1px solid #CCCCCC;
	background-color: #EEEEEE;
	padding: .5em;
	}
	th { padding-left: .75em; padding-right: .75em }
	li { margin-bottom: .5em }
	</style>
	</head>
	<body>

	<h1>Lambda Calculator - Exercise File Format</h1>

	<p>Exercise files created by the instructor are saved as plain-text files, usually with a <tt>.txt</tt> file extension. You can edit this files with, for instance, the Notepad program on Windows. When using Microsoft Word or another office suite, be sure to save the file as a Text Only-formatted file. When using special or international (non-ASCII) characters, files should be saved in the UTF-8 Unicode character encoding.</p>

	<p>An example exercise file is given below.</p>

	<pre>
	# Lines that begin with a hash are ignored.

	Homework 1

	constants of type e : a b-c
	constants of type <e,t> : P-Q
	variables of type e : x-z
	variables of type <et> : X Y

	exercise semantic types
	points per exercise 10
	title Semantic Types
	directions Give the semantic type of the following lambda-expressions.

	c
	P(c)
	Q(x) V ~Q(x)
	Lx[P(x) & Q(x)]

	exercise lambda conversion
	points per exercise 15
	title Lambda Conversion
	directions After checking that the type of the function and the type of the
	directions argument(s) match, simplify the following expressions performing
	directions one lambda-conversion at a time.

	Lx[P(x) & Q(x)] (a)
	LxLy[R(a,y) & Q(x)] (a) (b)
	Lx[a] (b)
	LxLx[P(x) -> R(x,c)] (a) (b)
	</pre>

	<h2>File Format Basics</h2>

	<p>Blank lines in execise files are ignored, and lines that begin with a hash (#) are also ignored. You can use hashes to store notes in the file that won't be read by the Lambda program, but of course keep in mind that students can view such notes if they open the exercise file in a text editor themselves.</p>

	<p>The first (non-ignored) line of every exercise file is the title of the exercise to be shown to the student, and for the instructor's use later when reviewing the students' work. In the example above, this is <tt>Homework 1</tt>.</p>

	<p>Following this line, a line is either a <i>directive</i> to the Lambda program, or it is an <i>exercise</i>.</p>

	<h2>Directives</h2>

	<p>Directives are lines that begin with specially recognized commands. These are explained below.</p>

	<dl>

	<dt><tt>constants of type ___ : ___</tt></dt>
	<dt><tt>variables of type ___ : ___</tt></dt>
	<dd>
	<p>These directives specify the typing convention for variables and constants found in the exercises. If none of these directives are present in an exercise file, the default type assignments shown below are used. The first time this directive is used in an exercise file, the defaults are cleared, and the new type assignments apply for all exercises following the directive.</p>
	<p>A type can be either:</p>
	<p>an atomic type, which can be any single letter,</p>
	<p>a complex (function) type specified as <T<sub>1</sub>,T<sub>2</sub>>, for types T<sub><i>i</i></sub>, or</p>
	<p>a cartesian-product type, specified as T<sub>1</sub>T<sub>2</sub>T<sub>3</sub>....</p>
	<p>One-place predicates are typed as complex types. Two-place (or more) predicates are typed as functions from a cartesian-product type to another type, i.e. as <tt><T<sub>1</sub>T<sub>2</sub>T<sub>3</sub>,T<sub>4</sub></tt>>. Commas may be omitted from complex types when the types on either side are both atomic.</p>
	<p>Examples:</p>
	<pre>
	constants of type e : a b-c
	constants of type <e,t> : P-Q
	constants of type <e*e,t> : R S T
	variables of type e : x-z
	variables of type <et> : X Y
	</pre>
	<p>These directives will always override previous uses of the directives, so you can change the typing conventions throughout the exercise file by issuing this directive again.</p>
	<p>The default typing conventions are:</p>
	<pre>
	constants of type e : a-e
	constants of type <e,t> : P-Q
	constants of type <e*e,t> : R-S
	variables of type e : u-z
	variables of type <et> : U-Z
	</pre>
	</dd>

	<dt><tt>points per exercise ___</tt><dt>
	<dd><p>This directive specified a numeric point value assigned to each exercise that follows the directive, or just until another <tt>points per exercise ___</tt> directive is found. The points value can be any rational number. It is up to the instructor to ensure that the total points add up to 100 if that is desired. Example:</p>
	<pre>points per exercise 15</pre></dd>

	<dt><tt>exercise ___</tt></dt>
	<dd><p>This directive begins a group of exercises and specifies the type of exercise in the group. The exercise type must be either <tt>semantic types</tt>, <tt>lambda conversion</tt>, or <tt>tree</tt>. These exercises are described below. The <tt>exercise ___</tt> directive <i>must</i> be followed by <tt>title ___</tt> and <tt>directions ___</tt> directives before any exercises are entered. Examples:</p><pre>exercise lambda conversion
	exercise semantic types
	exercise tree</pre></dd>

	<dt><tt>title ___</tt></dt>
	<dd><p>Specifies the title for the group of exercises. This directive must be specified after an <tt>exercise ___</tt> directive and before the actual exercises. Example:</p><pre>title Lambda Conversion</pre></dd>

	<dt><tt>directions ___</tt></dt>
	<dd><p>Specifies the directions to provide to the student for a group of exercises. This directive must be specified after an <tt>exercise ___</tt> directive and before the actual exercises. Directions can be split across multiple lines by repeating the <tt>directions ___</tt> directive. Example:</p>
	<pre>directions After checking that the type of the function and the type of the
	directions argument(s) match, simplify the following expressions performing
	directions one lambda-conversion at a time.</pre>
	<p>You can include predicate logic expressions inside the directions. By writing the expressions according to the directions below, and surrounding them in curly braces, they will appear to the student rendered nicely with the appropriate symbols for lambdas, etc.</p>
	<pre>directions The expression {Lx.Iy[P(y,x)]} has type <e,e>.</pre>
	<p>Greek letters may be included in two ways. 1) By preceding the name of the letter
	with a backslash, as in LaTeX. For instance, \alpha for lowercase alpha or \Omega for a capital omega. (Not all Greek letters are supported.)
	<!-- note something similar below within expressions and brackted trees -->
	2) By putting the special character directly within the text file (i.e. with
	Word's Insert Symbol), and saving the file in UTF-8 Unicode encoding.</p>
	<p>You can start a new paragraph in the directions by ending a line with
	two backslashes (\\), as in LaTeX.</p>
	</dd>

	<dt><tt>instructions ___</tt></dt>
	<dd><p>Specifies instructions for the following exercise only. This directive must be specified immediately before the exercise to which it applies. Instructions can be split across multiple lines and can include expressions in the same way as with the <tt>directions</tt> directive, described above. Example:</p>
	<pre>instructions This exercise is a trick question!
	Lx[a] (b)</pre></dd>

	<dt><tt>multiple letter identifiers</tt></dt>
	<dt><tt>single letter identifiers</tt></dt>
	<dd><p>After this directive, identifiers can be either be words of more than
	one letter, or may only be single letters. When the <tt>single letter identifiers</tt>
	directive is set, certain abbreviations are accepted when reading predicate
	logic expressions. For instance, "Pabc" may be used to abbreviate P(a,b,c).
	When <tt>multiple letter identifiers</tt>
	is used, "Pabc" is treated as a single identifier. If neither directive is
	specified, <tt>single letter identifiers</tt> is assumed.</p></dd>

	<dt><tt>define ___ : ___</tt></dt>
	<dd><p>Defines lexical entries for use in tree exercises provided to the student. The student will be able to enter other lexical entries as needed. Multiple words can be given the same lexical entry by separating the words with comma. A word may be given multiple lexical entries by repeating the <tt>define</tt> line multiple times. A single lexicon is used for all exercises in the file. Example:</p>
	<pre>define Sue : s
	define introduce, introduces : LxLyLz[introduces(z,x,y)]</pre></dd>

	<dt><tt>use rule ___</tt></dt>
	<dd><p>Indicates which composition rules are allowed to be used in tree exercises, including function application, non-branching nodes (copying the denotation of the single child node to the parent node), predicate modification, and lambda abstraction, based on the Heim & Kratzer textbook. Example:</p>
	<pre>use rule function application
	use rule non-branching nodes
	use rule predicate modification
	use rule lambda abstraction</pre></dd>


	</dl>

	<h2>Exercises</h2>

	<p>Lines that are not recognized as directives are assumed to be exercises, of the type specified in a preceding <tt>exercise ___</tt> directive.</p>

	<h3>Semantic Types Exercises</h3>

	<p>For this exercise type, the instructor enters an expression in predicate logic. The student's task is to provide the semantic type of the expression. For example, if the exercise is:</p>

	<pre>λx[P(x) ∧ Q(x)]</pre>

	<p>The student is expected to answer:</p>

	<pre><e,t></pre>

	<p>Or in an equivalent way, such as abbreviated as <tt>et</tt>.</p>

	<p>Predicate logic expressions can be entered in exercise files without needing to insert special characters like lambdas and wedges. This is described in more detail below. For the example above, the instructor enters into the exercise file:</p>

	<pre>Lx[P(x) & Q(x)]</pre>

	<p>The correct answer, i.e. the type of this expression, does not need to be entered into the exercise file. The Lambda program will compute the correct answer itself.</p>

	<h3>Lambda Conversion Exercises</h3>

	<p>For this exercise type, the instructor enters an expression in predicate logic. The student's task is to simplify the expression by performing lambda conversions, one at a time. For example, if the exercise is:</p>

	<pre>λx.λy[R(a,y) ∧ Q(x)] (a) (b)</pre>

	<p>The student is expected first to answer:</p>

	<pre>λy[R(a,y) ∧ Q(a)] (b)</pre>

	<p>The Lambda program will check this intermediate answer and then allow the student to proceed to the next step:</p>

	<pre>R(a,b) ∧ Q(a)</pre>

	<p>It is possible to lambda-convert over higher types. This proceeds as follows:</p>

	<pre>
	λX[X(b)] (λx. R(a,x))
	(λx[R(a,x)]) (b)
	R(a,b)
	</pre>

	<p>In addition, non-reducible predicate logic expressions may also be provided in the exercise file, such as the expression <tt>P(x)</tt>. In this case, the student is expected to respond with the same expression.</p>

	<p>Sometimes creating an alphabetical variant is needed before proceeding to lambda conversion. In these cases, the Lambda program will realize that an alphabetical variant is necessary, and it will require that the student enters it before preceeding with simplification. An example of this is shown below:</p>

	<pre>
	Exercise: λx.∃y[R(y,x)] (y)
	Student's responses:
	1) λx.∃yʹ[R(yʹ,x)] (y)
	2) ∃yʹ[R(yʹ,y)]
	</pre>

	<p>The correct answers to lambda conversion exercises, i.e. the simplifications of the expressions, do not need to be entered into the exercise file. The Lambda program will compute the correct answer (including the steps needed to reach it) itself.</p>

	<h3>How to enter predicate logic expressions</h3>

	<p>The Lambda program will read predicate logic expressions from exercise files. Predicate logic expressions may include:</p>

	<ul>
	<li>Constants and variables. Constants and variables must be single letters only, unless the <tt>multiple letter identifiers</tt> directive is used. Primes can be entered with the apostrophe. Some capital letters (A, E, I, and L) are treated specially by the Lambda program; see the note below on using these letters within constants and variables.</li>
	<li>Constants and variable with explicit types using an underscore to separate the name and the type, such as: x_e, X_<e,t>, etc. Composite types such as <e,t> must be written with brackets and cannot be abbreviated as "et". Explicit types are unnecessary when the typing conventions specified in the exercise file already provide a type for the identifier.</li>
	<li>Predicates, entered as P(a) or P(a,b,c) (or if the <tt>multiple letter identifiers</tt> has not been specified, in abbreviated form such as Pabc).</li>
	<li>The logical connectives, which can be entered according to the table below:
	<table>
	<tr><th>Connective</th> <th>You Type</th></tr>
	<tr><td style="text-align: center">¬</td><td style="text-align: center">~</td></tr>
	<tr><td style="text-align: center">=</td><td style="text-align: center">=</td></tr>
	<tr><td style="text-align: center">≠</td><td style="text-align: center">!=</td></tr>
	<tr><td style="text-align: center">∧</td><td style="text-align: center">&</td></tr>
	<tr><td style="text-align: center">∨</td><td style="text-align: center">V</td> <td>(capital letter v)</td></tr>
	<tr><td style="text-align: center">→</td><td style="text-align: center">-></td></tr>
	<tr><td style="text-align: center">↔</td><td style="text-align: center"><-></td></tr>
	</table>
	Operator precedence is as given in the table, except that the pairs →/↔, ∧/∨, and =/≠ represent operators at the same operator precedence, so expressions like (a = b ≠ c) is not well formed.</li>
	<li>Parenthesized expressions, using parens (...) or brackets [...].</li>
	<li>Quantifiers and binders, which can be entered using capital Roman letters according to the table below:
	<table>
	<tr><th>Quantifier</th> <th>You Type</th></tr>
	<tr><td style="text-align: center">∃</td><td style="text-align: center">E</td></tr>
	<tr><td style="text-align: center">∀</td><td style="text-align: center">A</td></tr>
	<tr><td style="text-align: center">λ</td><td style="text-align: center">L</td></tr>
	<tr><td style="text-align: center">ι</td><td style="text-align: center">I</td></tr>
	</table>
	For example, Ax[P(x)], AxEy[P(x) & Q(y)], Lx[P(x)], LxLy.P(x,y) & Q(y), Iz[king(z)]. Periods may separate multiple consecutive quantifiers/binders. After quantifiers and binders, a bracketed expression should follow to avoid scope ambiguity.</li>
	<li>To use capital E, A, L, I, and V as those letters in a constant or variable, precede the letter with a backslash (\) to indicate to the program to treat the letter following like normal, e.g. H\APPY, \L\ITT\L\E.</li>
	<li>Function application, which is an expression followed by another expression (usually in parenthesis and separated by a space), such as Lx[P(x)] (b).</li>
	<li>Single Greek letters may be used as constants or variables by preceding the name of the letter
	with a backslash, as in LaTeX. For instance, \alpha for lowercase alpha or \Omega for a capital omega. (Not all Greek letters are supported.)
	<!-- note use of Greek letters in directions and in bracketed trees --></li>
	<li>Numeric connectives, which can be entered according to the table below:
	<table>
	<tr><th>Connective</th> <th>You Type</th></tr>
	<tr><td style="text-align: center">⋅</td><td style="text-align: center">*</td> <td>(multiplication)</td></tr>
	<tr><td style="text-align: center"><</td><td style="text-align: center"><</td> <td></td></tr>
	<tr><td style="text-align: center">≤</td><td style="text-align: center"><=</td> <td></td></tr>
	<tr><td style="text-align: center">></td><td style="text-align: center">></td> <td></td></tr>
	<tr><td style="text-align: center">≥</td><td style="text-align: center">>=</td> <td></td></tr>
	</table>
	<li>Numbers can be entered and are treated as constants of type i.
	<li>Sets, set connectives, and set operators, which can be entered according to the table below:
	<table style="margin-bottom: 1em">
	<tr><th>Set Expression</th> <th>You Type</th></tr>
	<tr><td style="text-align: center">{ a, b, c, ... }</td><td style="text-align: center">curley braces and commas</td></tr>
	<tr><td style="text-align: center">{ x \| P(x) }</td><td style="text-align: center">curley braces and the pipe \| key</td></tr>
	<tr><td style="text-align: center">∅</td><td style="text-align: center">\emptyset</td></tr>
	</table>
	<table>
	<tr><th>Operator</th> <th>You Type</th></tr>
	<tr><td style="text-align: center">\| ... \|</td><td style="text-align: center">the pipe \| key</td> <td>(set cardinality)</td></tr>
	<tr><td style="text-align: center">∩</td><td style="text-align: center">^^</td> <td>(two carrets)</td></tr>
	<tr><td style="text-align: center">∪</td><td style="text-align: center">VV</td> <td>(two capital V's)</td></tr>
	<tr><td style="text-align: center">⊆</td><td style="text-align: center"><<</td> <td></td></tr>
	<tr><td style="text-align: center">⊈</td><td style="text-align: center">!<<</td> <td></td></tr>
	<tr><td style="text-align: center">⊊</td><td style="text-align: center"><<<</td> <td></td></tr>
	<tr><td style="text-align: center">⊇</td><td style="text-align: center">>></td> <td></td></tr>
	<tr><td style="text-align: center">⊉</td><td style="text-align: center">!>></td> <td></td></tr>
	<tr><td style="text-align: center">⊋</td><td style="text-align: center">>>></td> <td></td></tr>
	</table>
	<p>The intersection and union connectives bind more tightly than the other set and logical connectives.</p>
	<p>Note that the set notation { x \| P(x) } is a binder. All variables to the left of the vertical bar (which is usually just a single variable) bind occurrences of that variable to the right of the bar.</p></li>
	</ul>

	<h3>Tree Exercises</h3>

	<p>In tree exercises, the instructor provides a tree in labeled brackets notation. The student is presented with a graphical rendition of the tree and is expected to provide the denotations of the terminal nodes and to evaluate the denotations of the nonterminal nodes up to the root.</p>

	<p>To create a tree exercise, simply provide the brackets notation of the tree. To give nonterminal node labels, precede the label with a period. Nodes are not required to be labeled.</p>

	<pre>[.S [.NP John] [.VP [.V' loves] Mary] ]

	[ [the [fast man]] [ate [many apples]]]</pre>

	<p>Superscripts and subscripts may be indicated with the caret (^) and underscore (_). Only integer subscript indices are allowed. On nonterminals, these play no special role in the program. They are for pretty display purposes only.</p>

	<pre>[.DP_1 the [.NP_1 man [that_1 [I [ [.V^0 saw] t_1] ] ] ]]</pre>

	<p>Traces and pronouns with indices (t_<i>i</i>, he_<i>i</i>, she_<i>i</i>, it_<i>i</i>, him_<i>i</i>, her_<i>i</i>, himself_<i>i</i>, herself_<i>i</i>, itself_<i>i</i>, his_<i>i</i>, hers_<i>i</i>, its_<i>i</i>, theirs_<i>i</i>) are automatically given the denotation of g(1), g(2), etc. according to the index.</p>

	<p>Relative pronouns with indices (that_<i>i</i>, what_<i>i</i>, which_<i>i</i>, who_<i>i</i>, such_<i>i</i>) and bare indices (1, 2, 3, ...) are treated as "bare index" terminal nodes for lambda abstraction, following Heim & Kratzer.</p>

	<p>Single Greek letters may be used as terminal and nonterminal labels by preceding the name of the letter
	with a backslash, as in LaTeX. For instance, \alpha for lowercase alpha or \Omega for a capital omega. (Not all Greek letters are supported.)
	<!-- note use of Greek letters in directions and expressions--></li>

	</body>
	</html>