Request: once-and-for-all definitions of free-vars, free-in, not-free-in

[wilbowma]

I'll try to submit a patch in the coming weeks, but I'm going to leave this here for now in case someone knows how to do it more quickly than I do.

It seems like with the addition of binding-forms, we should be able to add a few more binding related (meta)functions "once-and-for-all", like was done for substitute and alpha-equivalent?.

In particular:

; Returns the free variables of any_e
free-vars : any_e -> (any_x ...)

; Returns #t when any_x is free in any_e, and #f otherwise.
free-in : any_e any_x -> #t or #f

; Returns #t when any_x is not free in any_e, and #f otherwise.
not-free-in : any_e any_x -> #t or #f

; Returns any_e with each any_xi replaced by any_ei. Substitution should be performed in order, so any any_e{i-1} can have any_xi.
; e.g.s
; (substitute* x (x y) (1 2)) -> 1
; (substitute* x (x y) (y 1)) -> 1
; (substitute* (x y) (x y) (1 2)) -> (1 2)
substitute* : any_e (any_xi ..._0) (any_ei ..._ 0) -> any_e

[paulstansifer]

There's no particular reason for them not to exist.

Do you have a use for them? I'm curious, because my (probably inaccurate) mental model for how metaprogrammers work is that they are interested in what names could be free in an expression, which is determined by the binding forms that it will be wrapped up in later on.

It should be pretty easy to nuke all bound variables with rec-freshen, similar to how canonicalize works:

(define (nuke-bound-vars language-bf-table match-pattern redex-val)
  (parameterize
   ([current-bf-table language-bf-table]
    [pattern-matcher match-pattern]
    [all-the-way-down? #t]
    [name-generator (λ (orig) `())])
   
(first (rec-freshen redex-val #f #t #f))))

Then all you'd need to do is flatten and remove duplicates. This might say that (lambda (x) x) has lambda as a free variable; I forget whether that's desirable in Redex.

[wilbowma]

I need these. I'm currently modeling several (complex) languages and compilers between them, and I need free-in and not-free-in in the type system, and free-vars in the compilers.

I wouldn't want keywords included, but it would be easier to write a wrapper that removes keywords than to write the massive boring fold over the language forms.

[wilbowma]

About keywords, might be related to #62. If there was a system to know whether or not lambda was a keyword/literal, then it could easily be excluded.

[rfindler]

@wilbowma I think that it may be the case that if you show a simplified example of why these free variable functions are useful in something like the type system you have in mind, it would help us understand and either make suggestions about your larger model or fix Redex.

[wilbowma]

For not-free-in, see https://github.com/wilbowma/cic-redex/blob/master/cic.rkt#L642

This is a model of the Calculus of Inductive Constructions (CIC), the core language of Coq. The definitions of strict positivity uses not-free-in to determine if a type t is considered a recursive argument and must be restricted to a strictly positive use. A type is a recursive argument if the inductive type D being defined appears, as a free variable, in the type t. This is a fairly literal translation of the specification given in the Coq manual, https://web.archive.org/web/20150326181604/https://coq.inria.fr/doc/Reference-Manual006.html, section 4.5.3.

That model also includes subst-all, an n-ary version of substitute, which I've now defined about 5 times and should probably be included in a standard library somewhere.

(I know you asked for a simplified example. I'm sorry to say that is the simplified example.)

[rfindler]

Thanks.

Is something like this what you have in mind (to be used in the first case of "X occurs strictly positively in T" in the web.archive.org link)? (perhaps negated?)

(define-metafunction λL
  free-in : x e -> boolean
  [(free-in x x) #t]
  [(free-in x (e ...))
   (where (boolean_1 ... #t boolean_2 ...) ((free-in x e) ...))]
  [(free-in x e) #f])

[rfindler]

Oops, this is probably closer to the code I had in mind:

(define-metafunction λL
  free-in : x e -> boolean
  [(free-in x x) #t]
  [(free-in x (e ...))
   #t
   (where (boolean_1 ... #t boolean_2 ...) ((free-in x e) ...))]
  [(free-in x e) #f])

[wilbowma]

That's a better implementation than mine, I think, but yeah that's basically it.

[howell]

Chiming in to say that I wrote a subst-all the other day as well. My use case was pattern matching, building up an explicit substitution while walking over a value and pattern and then applying it all in one go to the match-successful-expression.

[leafac]

I’m also interested in free-vars. My use-case is m-CFA:

Page 312