Lambda calculus with generalized abstraction

Lately I’ve been thinking about this: What do we get if we change lambda calculus’s abstraction from (λx.M) to (λN.M), where M and N are lambda terms, and x is a variable?

That is (following the structure from my previous post), our new syntax becomes:

<var>   ::= x
<abs>   ::= λ<term>.<term>
<app>   ::= <term><term>

<term>  ::= <var> | <abs> | <app>
<value> ::= <abs>

In Haskell code:

type VarName = String
 
data Term =
    TmVar VarName
    | TmAbs Term Term
    | TmApp Term Term deriving (Eq, Show)

With the new list of inference rules:

Name	Rule
E-App1	$\frac{t_1 \to t_1'}{t_1t_2 \to t_1't_2}$
E-App2	$\frac{t_2 \to t_2'}{v_1t_2 \to v_1t_2'}$
E-App3	$\frac{t_2 \to t_2', v_1t_2' \to v_1'}{(\lambda v_1.t_{12}) \ t_2 \to \lambda v_1'.t_{12} }$
E-AppAbs	$(\lambda x.t_{12})v_2 \to [x \mapsto v_2]t_{12}$

So the evaluator looks something like:

eval : Term -> Term
eval (TmApp (TmAbs (TmVar x) t12) v2)      = subst x t12 v2 -- E-AppAbs
eval (TmApp (TmAbs v1@(TmAbs _ _) t12) t2) = let t2' = eval t2 in let v1' = eval (TmApp v1 t2') in TmAbs v1' t12 -- E-App3
eval (TmApp v1@(TmAbs _ _) t2)             = let t2' = eval t2 in TmApp v1 t2' -- E-App2
eval (TmApp t1 t2)                         = let t1' = eval t1 in TmApp t1' t2 -- E-App1
eval (TmVar x)                             = TmVar x -- E-Var
eval x                                     = error ("No rule applies: " ++ show x)

subst is the same as in the previous post.

So with this system we could “control” the “arguments” in the abstraction through application.
We could represent λx.x and λy.x through a single abstraction, i.e. (λ(λx . x) . x) so we get to either pass x or y to it:

Main> let f1 = TmAbs (TmVar "x") (TmVar "x")
Main> let f2 = TmAbs (TmVar "y") (TmVar "x")
Main> let f3 = TmAbs (TmAbs (TmVar "x") (TmVar "x")) (TmVar "x")
Main> eval (TmApp f3 (TmVar "x")) == f1
True
Main> eval (TmApp f3 (TmVar "y")) == f2
True

Is this useful or not? I didn’t know 🙂 so as always I referred to ##dependent@freenode and learned a bunch of new stuff:

 <pgiarrusso> I suspect many metaprogramming facilities would allow generating `𝜆 foo. x` by picking `foo`, but I don't see any reason to support this specifically
 <pgiarrusso> to be sure, I'm not necessarily saying "there is no point"
 <pgiarrusso> also, for your example, it seems `if foo then λx.x else λy.x` would work as well
 <pgiarrusso> my best answer is, when you write a function, you want to know what are the function params, to refer to them

Some stuff on papers:

 <pgiarrusso> *now*, I'm sure that strange variants of LC exist which do make sense but look surprising
 <pgiarrusso> but I think people usually start from something that is (1) useful but (2) hard, and then build a formal system to support that
 <pgiarrusso> s/people/researchers/
 <bor0> how do they know that it's useful?
 <pgiarrusso> sometimes you do go the opposite way, but that's harder
 <pgiarrusso> bor0: take a PL paper, read the introduction, see the arguments they make
 <bor0> I don't understand how that determines the usefulness of the paper itself?
 <bor0> or the idea even
 <pgiarrusso> bor0: not sure what paper to pick, but http://worrydream.com/refs/Hughes-WhyFunctionalProgrammingMatters.pdf might be an example
 <pgiarrusso> lots of that paper is an argument that lazy evaluation is interesting and useful
 <pgiarrusso> it does not *prove* that it's useful, as that's not something you can prove
 <pgiarrusso> but that paper (and many others) show something that is hard to do, arguably desirable, and give a "better" way of doing it

Bonus 🙂

 <mietek> bor0: <gallais> Someone was talking about a lambda calculus with full terms instead of mere variables in binding position IIRC
 <mietek> bor0: <gallais> I just came across this work: https://academic.oup.com/jigpal/article/26/2/203/4781665
 <bor0> wow thanks mietek!
 <bor0> interesting how when humans think about a certain topic they almost always have overlapping ideas
 <bor0> (:philosoraptor: it just confirms Wadler's statement that mathematics is discovered, not invented, I guess)
 <bor0> but I am happy that I had thought of that, even if for 2 years late (article was published in 2017)

Update: Thanks to /u/__fmease__ for noticing an error in the E-App3 LaTeX rule.

2 thoughts on “Lambda calculus with generalized abstraction”

jukowah says:

11/12/2022 at 09:49

Thank you for the this post, very interesting topic. But this shouldn’t increase the expressive power, right? At least in a capture avoiding language, unless there is some support for sort of first class names, if that’s a thing. Anyway, it’s a really interesting extension to traditional lambda calculus none the less. And I’m curious, have you made any progress in this or could you find some resources about it and extending it with types?

LikeLike

1. Boro Sitnikovski says:
  
  12/12/2022 at 08:43
  
  > But this shouldn’t increase the expressive power, right?
  
  Yes, as pointed out by pgiarrusso, `if foo then λx.x else λy.x` captures this.
  
  > have you made any progress in this
  
  I have not taken it further, it was just a small experiment, but I myself am also curious if there are any other useful applications to the idea 🙂
  
  LikeLike