Stream: new members

Topic: lambda calculus implementation in lean

Miguel Negrão (Jun 16 2023 at 08:12):

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 (Jun 16 2023 at 19:56):

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 (Jun 16 2023 at 23:43):

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.

docs4#Set

Kevin Buzzard (Jun 17 2023 at 00:11):

Looks like it's in mathlib4

Scott Morrison (Jun 17 2023 at 08:10):

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 (Jun 17 2023 at 09:36):

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 (Jun 17 2023 at 09:39):

No because it might be uncountably infinite

Ruben Van de Velde (Jun 17 2023 at 09:41):

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

Yaël Dillies (Jun 17 2023 at 09:41):

Countably uninfinite? :upside_down:

Kevin Buzzard (Jun 17 2023 at 09:43):

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 (Jun 17 2023 at 09:59):

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

Kevin Buzzard (Jun 17 2023 at 10:07):

Yeah you can't get uncountable finsets :-)

Miguel Negrão (Jun 17 2023 at 11:11):

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

Ruben Van de Velde (Jun 17 2023 at 11:24):

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 (Jun 17 2023 at 11:28):

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

Jireh Loreaux (Jun 17 2023 at 16:09):

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

Jireh Loreaux (Jun 17 2023 at 16:10):

What inductive definition of Finest are you imagining, exactly?

Miguel Negrão (Jun 20 2023 at 10:36):

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 (Jun 20 2023 at 10:43):

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 (Jun 20 2023 at 11:02):

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

Miguel Negrão (Jun 20 2023 at 11:12):

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 (Jun 20 2023 at 11:26):

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 (Jun 20 2023 at 12:13):

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 (Jun 20 2023 at 12:53):

@Kevin Buzzard got it, thanks !

Kyle Miller (Jun 20 2023 at 17:21):

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

Kyle Miller (Jun 20 2023 at 17:29):

@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 (Jun 20 2023 at 17:49):

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 (Jun 20 2023 at 22:07):

@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.)

Kyle Miller (Jun 20 2023 at 22:12):

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 (Jun 20 2023 at 22:28):

Agreed. See !4#3878 for related discussion.

Last updated: Dec 20 2023 at 11:08 UTC