Documentation

Dylan Bumford edited this page Dec 14, 2015 · 4 revisions
Clone this wiki locally

The Lambda Calculator

Documentation

For students and instructors: When typing predicate logic expressions in the program, some special keyboard combinations are used to enter logical symbols. See the special symbols guide for entering special symbols for instructions. Some help is also provided within the program.

For Instructors: If you would like to write an exercise file, you may read the exercises file documentation for the exercise file format or consult the example0.txt complete and documented sample exercise file for instructors

A Note on Operator Precedence

Binding Domains

The scope of binding operators extends as far to the right as possible, within the binder's nesting group.

  • ∀x.P(x) ∧ Q(x) is parsed as [∀x[P(x) ∧ Q(x)]]
  • λyλx.f(x)(a) is parsed as [λy[λx[f(x)(a)]]]

Importantly, brackets are used only for grouping; they do not delimit scope.

  • ∀x.[P(x) ∧ Q(x)] ∧ R(x) is parsed as [∀x[[P(x) ∧ Q(x)] ∧ R(x)]]
  • λyλx.[f(x)](a) is parsed as [λy[λx[f(x)(a)]]]

The dot following the binder is purely aesthetic, as is white space. However, unless the exercise explicitly declares single letter identifiers, there will need to be some indication as to when the binding prefix ends and the body of the lambda term begins.

All of the following are parsed as [λy[λx[f(x)(a)]]].

  • λyλx.f(x)(a)
  • λyλx f(x)(a)
  • λyλx[f(x)(a)]
  • λyλx. f(x)(a)
  • λyλx.[f(x)(a)]
  • λyλx [f(x)(a)]
  • λyλx. [f(x)(a)]
  • λyλxf(x)(a) (will not work unless single letter identifiers declared)

Connectives

Within a nesting group, the following precedence among logical connectives are imposed:

  1. ¬
  2. ∩, ∪, ⊕
  3. =, ≠, <, ≤, ⊆, ⊑
  4. ∧, ∨, →, ↔

Some examples

  • S ∩ T = Y is parsed as [[S ∩ T] = Y]
  • X ⊕ T ⊑ Y is parsed as [[X ⊕ T] ⊑ Y]
  • ¬p ∨ q = r [[¬p] ∨ [q = r]]
  • ¬p ∨ q → r is ambiguous and will not parse
  • ¬p ∨ [q → r] is parsed as [[¬p] ∨ [q → r]]