lambda calculus implementation in lean

Stream: new members

[Miguel Negrão]

Hi all, is there a recommended implementation of lambda calculus in lean ? Can be either the untyped or simply typed, named variables or with indexes. thanks !

[Miguel Negrão]

And a somewhat unrelated question (but related to implementing a function for free variables in a term), does Lean or the Std library(version 4) have sets, i.e., colections without duplicates, or do I need mathlib ?

[Miguel Negrão]

Is it the case that set was part of Lean 3 but was removed in Lean 4 ? I find it in the docs for lean 3 (https://leanprover-community.github.io/mathlib_docs/init/data/set.html#set) but not for lean 4.

[Kevin Buzzard]

docs4#Set

[Kevin Buzzard]

Looks like it's in mathlib4

[Scott Morrison]

Lean 4 core has an extremely minimal library: what is needed for the language itself. Std4 is intended to be a standard library, i.e. just the intersection of what mathematicians and programmers might want. Set is not exactly a "collection" in the programming sense, so I think it correctly belongs in mathlib for now.

[Miguel Negrão]

Great, thanks ! Is it not possible to display the contents of a set ?

def set1 : Set ℕ := { 0 }

def set2 : Set ℕ := set1 ∪ { 0 }

#eval set2
def set1 : Set ℕ := { 0 }

def set2 : Set ℕ := set1 ∪ { 0 }

#eval set2

[Kevin Buzzard]

No because it might be uncountably infinite

[Ruben Van de Velde]

Can a set of naturals be uncountably infinite? Still, countably infinite might be an issue too

[Yaël Dillies]

Countably uninfinite? :upside_down:

[Kevin Buzzard]

I was explaining why you can't hope for there to be a general function which prints sets. No, no set of naturals can be uncountably infinite.

[Miguel Negrão]

Ok, I think Finset is enough for what I need, and that I can print.

[Kevin Buzzard]

Yeah you can't get uncountable finsets :-)

[Miguel Negrão]

Is it possible to convert a Finset String to List String ?

[Ruben Van de Velde]

You'll need to define some order, but then https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finset/Sort.html#Finset.sort should work

[Miguel Negrão]

And it is not possible to do structural recursion on a Finset, is it ?

[Jireh Loreaux]

No, but there is docs4#Finset.induction_on for proving.

[Jireh Loreaux]

What inductive definition of Finest are you imagining, exactly?

[Miguel Negrão]

Something with empty and Finset.cons, but I imagine that as @Ruben Van de Velde mentioned that would require some specific order for the elements.

[Kevin Buzzard]

That doesn't give you finite sets because a :: b is different to b :: a and a is different to a :: a. Unless you're using a nonstandard definition of "finite set".

[Miguel Negrão]

I think Finset.sort is the way to go for what I wanted.

[Miguel Negrão]

with Finset.cons a :: {b} and b :: {a} are the same set:

def finset5 : Finset ℕ := {2}
def finset6 : Finset ℕ := {1}

def finseth2 : ¬ 1 ∈ finset5 := by simp only []
def finseth3 : ¬ 2 ∈ finset6 := by simp only []

def finset7 : Finset ℕ := Finset.cons 1 finset5 finseth2
def finset8 : Finset ℕ := Finset.cons 2 finset6 finseth3

def finseth4 : finset7 = finset8 := by simp

[Ruben Van de Velde]

The order is needed to convert a finset to a list in a reproducible way, not so much for doing other things with it. Not sure I made that clear before

[Kevin Buzzard]

Miguel Negrão said:

with Finset.cons a :: {b} and b :: {a} are the same set:

def finset5 : Finset ℕ := {2}
def finset6 : Finset ℕ := {1}

def finseth2 : ¬ 1 ∈ finset5 := by simp only []
def finseth3 : ¬ 2 ∈ finset6 := by simp only []

def finset7 : Finset ℕ := Finset.cons 1 finset5 finseth2
def finset8 : Finset ℕ := Finset.cons 2 finset6 finseth3

def finseth4 : finset7 = finset8 := by simp

Yes absolutely, with mathlib's (non-inductively defined) finsets, but the question was "what inductive definition of Finset are you imagining" and your answer was "something with empty and Finset.cons", and my point is that if you define Finset to be an inductive type with those constructors (which is what you would have to do to make the concept of structural recursion even make sense) then the code above won't work.

[Miguel Negrão]

@Kevin Buzzard got it, thanks !

[Kyle Miller]

There's definitely a Finset.cons induction principal though: docs4#Finset.cons_induction

[Kyle Miller]

@Miguel Negrão What are you doing with Finset? If you find you need Finset.sort to turn them into lists, that suggests to me it might be the wrong type. They're not the best (though not the worst) for doing actual computations, and depending on what you're doing you might be better served by something else.

It would be nice if we had a version of Finset that was for ordered types, where the terms are strictly increasing lists of elements. (So, a subtype rather than a subtype of a quotient type.) There are better structures still in this case; I think red-black trees would give better all-around performance, though a tradeoff is that there are multiple representations of the same set as a red-black tree so you'd need quotients again to get them to be mathematical finite sets.

[Miguel Negrão]

I was trying to implement the evaluation of expressions in the untyped lambda calculus ULC, for my own learning. I was using variables with names, and was trying to generate new names when doing substitution if needed for bound variables. I was using Finset for the set of free variables. I think I will just use de bruijn indexes, seems easier to implement.

[Yaël Dillies]

@Kyle Miller said:

It would be nice if we had a version of Finset that was for ordered types, where the terms are strictly increasing lists of elements. (So, a subtype rather than a subtype of a quotient type.)

docs4#StrictSeries ?

[Kyle Miller]

That's mathematically fine, but for computation you'd rather have a concrete List rather than a function so that the data is actually stored somewhere.

[Yaël Dillies]

Agreed. See !4#3878 for related discussion.