What is free term in Aya note?

[illusory0x0]

This free term seems to have the same definition as Lambda Calculus Wikipedia's closed term, so where does this terminology come from? Why not use closed term?

An expression that contains no free variables is said to be closed. Closed lambda expressions are also known as combinators and are equivalent to terms in combinatory logic.

note/free-term.md

[ice1000]

I see the ambiguity here. Wikipedia LC only considers raw lambda terms, while Aya terms have the notion of "context", and we have syntactic differences between free vs. non-free variables (non-free variables are represented as De Bruijn indices).

I recommend reading about "locally nameless", which is discussed in the Wikipedia page of De Bruijn indices.

Once you learned about that, it becomes clear. If you have something that's meant to be a closed term, but you take the terms under the binders out, you get something illegal -- and we need to apply some operations immediately to legalize it. Those are called bound terms. Non-bound terms are naturally called free terms, because they use either free variables or use locally-bound variables.

Maybe the notes can be revised to clarify this.

[ice1000]

注意：这个术语指的不是 class FreeTerm，用于表示自由变量的 Term

So where exactly do you see the syntactic difference you mentioned?

Syntactic difference means they are different ASTs

[ice1000]

Free term is not a representation, but a property of terms.

[ice1000]

I see the ambiguity here. Wikipedia LC only considers raw lambda terms, while Aya terms have the notion of "context".

So the terminology free term is very similar to closed term, but does free term describe this meaning more precisely than closed term?

The word closed terms only makes sense when you use identifiers (like strings or unique IDs) to represent variables. Once you use LN you will have different kinds of non-closed terms, and when you say closed it's unclear what you mean.

[illusory0x0]

Once you use LN you will have different kinds of non-closed terms, and when you say closed it's unclear what you mean.

There are some OCaml code to clasify this concept. This is actually unrelated to local nameless; it's more about the concept of "local" rather than a specific nameless representation.

(* 
 * `Fun.id 0` is closed term.
 * `Fun.id` is defined term.
 *)
Fun.id 0;;
- : int = 0

(*
 * `id 0` is a term contains free variable, not the closed term.
 * `id` is bound term.
 *)
 let main id =
          id 0;; 

[ice1000]

That Fun.id is likely a defined variable. It has nothing to do with locally nameless

[illusory0x0]

@ice1000 I found better terminology for the free term notion, we can use defined term to represent free term notion. maybe bound variable and defined variable would be better.

• section 9.1 Extension of lambda C to the system lambda D, introduce delta context and gamma context for bound variable and defined variable.

• elaz-zoo also use BD to distinguish this different variable for different context. source location

reference: 《Type Theory and Formal Proof: An Introduction》, Nederpelt, Rob , Chapter: Extension of lambda C with definitions.

[ice1000]

I think defined term is far from intuitive....

[illusory0x0]

I think defined term is far from intuitive....

I think free term note is not clear enough and it would be better to directly quote from "Type Theory and Formal Proof: An Introduction," Nederpelt, Rob, Chapter 9: Extension of lambda C with definitions. It explains it in great detail.

This description is misleading. eafa62e#diff-ec20477db0c958cfd6110b4df1392b7450d206e1ded1a4996d31c0486887a894

[ice1000]

Just thought about it. We have delta context and delta reduction too. Those are unrelated to free terms. Those are defined variables, called DefVar in the code.

It will be important to know what defined variables are used for, so you will not be confused.