Hardegree, Formal Semantics, Homework #2page 1 of 2

Exercises on Monadic Lambda-Abstraction

1.Lambda-Conversion

The lambda-conversion rule for monadic lambda-abstracts can be stated as follows.

[v] // [/v]

Here,  and  are any expressions, v is any variable of the same type as , and
[/v] results when  replaces every free occurrence of v in ,
where v is free for in ,
which is to say that any variable that is free in  is also free in [/v].

Here, I use the meta-linguistic symbol ‘//’ to indicate that the two sides are interchangeable in all contexts.

2.Alphabetic Variance

Because of the restrictions on substitution in -conversion, sometimes one cannot substitute the expression for the variable v in , but must first apply the rule alphabetic variance to .

Alphabetic Variance (AV) [simple form]
[u] // [v]
Here, u, v are variables, [u], [v] are expressions, and
[u] is the result of substituting u for every bound occurrence of v in [v],and
[v] is the result of substituting v for every bound occurrence of u in [u].
An occurrence of a variable  is bound iff that occurrence lies within the scope of an operator binding  – i.e., , , , . Otherwise, that occurrence is free.
A variable  is free in an expression  iff at least one occurrence of  in  is free in .
Alphabetic Variance (AV) [general form]
1 // 2
Here, 1 , 2 are expressions that result from each other by bound-variable permutation. In other words, there is a permutation (1–1 function)  on the class Vof variables,whose inverse is –1, such that:
1 is the result of substituting (u) for every bound occurrence of u in 2, and
2is the result of substituting –1(v) for every bound occurrence of v in 1.
Examples / Non-Examples
F // F / F // F 
R // R / R // R 
R // R / R // R

3.Official Functor-Argument Notation

Officially, every (monadic) functor-argument compound is written as follows.

[functor]argument

However, we adopt variations and abbreviations in keeping with intermediate logic, without mention, as follows.

(1)Square-brackets may be deleted if the functor is simple.

(2)Corner-brackets may be deleted if the argument is simple, unless the functor is simple and has the same height as the argument.

(3)Corner-brackets may be replaced by round-parentheses or square-brackets in accordance with intermediate logic.

4.Bracket Shorthand (left association– LA)

[][[]]

Examples,

[R]ab[[R]a]b

[R]abc[[[R]a]b]c

5.Type Conventions

un-bolded / bolded
lower-case Roman letters / variables of type D / proper-expressions of type D
upper-case Roman letters / variables of type DS / proper-expressions of type DS

6.Exercises

Evaluate the following expressions using lambda-conversion (C), plus AV and LA as needed, showing all intermediate steps, including annotation (LA,C,AV) placing each step on its own line.

Compute inside-out.
Equally-inner computations can be done simultaneously.

(1)[R]a

(2)[R]ab

(3)[R]abc

(4)[[R]a]b

(5)[[[R]a]b]c

(6)[PP]R

(7)[P{Pa& Pb}]Rc

(8)[PQ{PQ}]RRa

(9)[P{PR}]Ra

(10)[[PQ{PQ}]KH]a