# Zulip Chat Archive

## Stream: new members

### Topic: lambda-terms by S, K combinators

#### Horatiu Cheval (Feb 15 2021 at 07:22):

Hello, I am trying to implement a version of the SKI calculus, and I got stuck at defining λ-terms by combinators. What I have is

```
inductive type
| ground : type
| compose : type → type → type
infixr `>>` := type.compose
-- for each type τ, variables of type τ are represented by natural indices
inductive var (τ : type)
| mk : ℕ → var
inductive term : type → Type
| of_var : ∀ {τ : type}, var τ → term τ
| app : ∀ {τ σ : type}, term (τ >> σ) → term τ → term σ
| K : ∀ {τ σ : type}, term $ τ >> σ >> τ
| S : ∀ {τ σ ρ : type}, term $ (τ >> σ >> ρ) >> (τ >> σ) >> τ >> ρ
-- is_free_var x t means that x occurs in t
-- Probably needed for the following definition, I left out its body
inductive is_free_var : ∀ {τ σ : type}, var σ → term τ → Prop
instance decidable_is_free_var : ∀ {τ σ : type} {t : term τ} {x : var σ}, decidable $ is_free_var x t := sorry
```

Now, for variables `x`

and terms `t`

of any type, we define a term`λ x . t`

by

`λ x . x := S K K`

`λ x . a := K a, if x is not a variable in a`

`λ x . (a x) := a, if x is not a variable in a`

`λ x . (a b) := S (λ x . a) (λ x. b), otherwise`

for combinators of appropriate types. I've been trying for some time to implement this definition

```
def lambda : ∀ {τ σ : type}, var τ → term σ → term (τ >> σ) := sorry
```

The main problem is that the definition does not follow the inductive structure of terms, so I end up with a lot of nested case-checks (which can't even be easily written for variables, since I cannot write x = y with x : var τ and y : var σ), which end up not typechecking, or rendering Lean unable to prove the recursions are terminating or other errors. I can post some of my unsuccessful attempts if it helps. Am I missing a cleaner way of writing this definition?

Last updated: May 08 2021 at 18:17 UTC