Description

This software provides a tool to compute lambda expressions in the simply typed version of LC. Computations are done only by mean of syntactic substitution.

Formal grammar

Symbols

\(Raw\; Types\; \mathbb{t} = \{nat, char, bool, empty\}\)

\(Constants: \mathbb{C} = \{O, 'a\dots z', true, false, null\}\)

\(Operators = \{lambda, apply, pi, first, second, succ\}\)

In addition, we have an infinite set of dummy names called \(\mathbb{n}\).

\(Types\; \mathbb{T} = \{x | x \in \mathbb{t} \lor \exists A, B \in \mathbb{T}, x = A\times B \lor \exists A, B \in \mathbb{T}, x = A\rightarrow B)\}\)

Syntax rules

The set of well formed expression is named \(\mathbb{E}\).

\(x \in \mathbb{C} \Rightarrow x \in \mathbb{E}\)

\(E \in \mathbb{E},\; x \in \mathbb{n} \Rightarrow lambda\; x\; E \in\ \mathbb{E}\)

\(E1,\; E2 \in \mathbb{E},\; E1:A\rightarrow B,\; E2:A \Rightarrow apply\; E1\; E2 \in \mathbb{E}\)

\(E1, E2 \in \mathbb{E} \Rightarrow pi\; E1\; E2 \in \mathbb{E}\)

\(E \in \mathbb{E},\; E:nat \Rightarrow succ\; E \in \mathbb{E}\)

\(E \in \mathbb{E},\; E:A\times B \Rightarrow first\; E \in \mathbb{E}\)

\(E \in \mathbb{E},\; E:A\times B \Rightarrow second\; E\; \in \mathbb{E}\)

Typing rules

• Abstraction rule:

\(\Gamma, x:A, E:B \vdash lambda\; x\; E: A\rightarrow B\)

• Application rule:

\(\Gamma, E1:A\rightarrow B, E2:A \vdash apply\; E1\; E2:B\)

• Pair introduction:

\(\Gamma, E1:A, E2:B \vdash pi\; E\; E:A\times B\)

• Pair elimination right:

\(\Gamma, E:A\times B \vdash first\; E: A\)

• Pair elimination left:

\(\Gamma, E:A\times B \vdash second\; E: B\)

• Successor rule:

\(\Gamma, E:nat \vdash succ\; E:nat\)