Zulip Chat Archive

Stream: new members

Topic: lambda-terms by S, K combinators

view this post on Zulip 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