[Question]
  [
*The goal of this challenge is to fill a niche that is mostly lacking on this site. In my observations there most parsing verification challenges fall into two categories:*
1. Super easy parsing. This parsing can usually be done with a regex, and regex based answers usually do well.
2. Super complex parsing. These are challenges with a lot of small parsing components that would on their own be type 1, but together make for long code with a lot of edge cases.
Neither of these categories are really bad, each can have fun challenges, but I want to shoot for something different. A challenge which is hard, hard enough that a regex will be unable to do the brunt of the work but with an easy to understand spec.
---
The goal of this challenge is to parse a *lisp-like* lambda function. Your code should accept a string as input and output of two possible consistent values. One which corresponds to an affirmative response (i.e. the input is a properly formatted lambda) and the other corresponds to a negative response (i.e. the input is *not* a properly formatted lambda). The string will only contain lowercase letters, spaces and parentheses (`(` or `)`).
I've put together 3 specifications of what constitutes a validly formatted lambda for this challenge. The first is a quick intuition base explanation. It explains the process and what things mean even if it is not perfectly rigorous. The second a formal grammar which expresses the idea succinctly and with no ambiguity. And the third is raw code, which is the hardest to read for humans but allows you to play around with the idea by trying different inputs. I recommend you read one of the first two and play around with the third.
## Formatting
The challenge uses a lisp like format. This consists of "lists" which are just parentheses enclosing lowercase words, and other lists separated each by exactly one space. So
```
(foo (bar baz) foobar)
```
Would be a lisp-like "list". For our challenge each list will be identified by it's first element (which should by highlighted by the syntax highlighter), which must be either `app`, `abs`, or `var`, representing applications, abstractions and variables, respectively.
An application is the application of one lambda function to another. It is represented by a three element list starting with of course `app` followed by two other valid lambda expressions. So if `S` and `K` were valid lambdas then:
```
(app S K)
```
would be a valid lambda too.
The other two abstractions and variables work together, an abstraction introduces new names for variables and variables use those names. An abstraction encloses some lambda which must be valid with the introduced variable name, and a variable can only use names which are given by abstractions that surround it. So
```
(abs x (abs y (var x)))
```
Is valid because the `x` name was introduced and used in a nested context. But
```
(app (abs x (var x)) (var x))
```
Is not because even though there is an abstraction for `x` the second `(var x)` is not surrounded by any abstraction at all, let alone one that introduces `x`.
Additionally abstractions can only introduce *new* variables, so
```
(abs x (abs x (var x)))
```
is not valid because the name `x` is ambiguous, it could refer to either abstraction. Variable names must be a string of lowercase ascii letters (`a`-`z`).
## Grammar
Now for the golfy definition. This parse cannot be defined in terms of a context free grammar, so this grammar uses context. The context is a set of strings of lowercase ascii letters (these are the valid variable names) and is represented here with \$C\$. To start \$C\$ is empty.
\$
S\left(C\right) := \left\{
\begin{array}[rr] \
\color{green}{\texttt{(var }}x\color{green}{\texttt{)}} & \textrm{ where } x\in C \\
\color{green}{\texttt{(abs }} x\texttt{ }S(C\cup\{x\})\color{green}{\texttt{)}} & \textrm{ where } x\notin C\\
\color{green}{\texttt{(app }} S(C)\texttt{ }S(C)\color{green}{\texttt{)}} &
\end{array}
\right.
\$
Any string spanned by the grammar from \$S(\{\})\$ is valid and any string not is invalid.
## Code
```
lambda :: [String] -> Parser ()
lambda variables =
  do
    char '('
    choice
      [ do
        string "abs "
        name <- some $ charBy (`elem` ['a'..'z'])
        guard $ notElem name variables
        char ' '
        lambda (name : variables)
      , do
        string "var "
        choice (map string variables)
        return ()
      , do
        string "app "
        lambda variables
        char ' '
        lambda variables
      ]
    char ')'
    return ()
```
[Try it online!](https://tio.run/##pVRNa@MwEL3nVwylYImmhuYYmkBbdm@FhT1mTaskcmLWX8iKmyz979mRNFIUp90e9mJJM2@e3nzIW9H9lmV5LKq2URqemlqrpkwf2rYsVkIXvRwBMCiLXD9McDuGh1JLVVsXsDTlaOSjQfhzU4u1DdzshFpbyKiWb/rQSvghVCcVCJihnQ7sp1ZFvYHbOSxoPwbBMwwTKOUA0@kpDkGfwAnMCNpy6OwtLa6jUVF3WtQrCd939Uo3yjO@baUyaeaVaCFHX0xgwoPMa4dh9hPgnEMbsUe1G97Q7pSE/Tkng1/QRel0lM6eZ6ZqQLWH/KTqjp/2k3OJdgsD0nVDZnQoWd2NQckOSe5vkYtwZ4iJRUwcYgImJviV1DtVe1huqRyaIDyqhR2EYRW8dJjPZ0jwX/KH6mkAcoJEymNZ8QwPxMmq1YfLDr3Y5piOAEQp3MH9@zycJsNpOc8j1BpubgyYDihstRXq0Q45e8KtAT82TcnNhsiM3eNaJddmwmT8hDamSj4LwCMwAVNY@vkAWABbmmcC7xGDgMzjMb0AzZwoI8krGgqhQSZNbD@bYSaUE4adnigFOoNHmFCtRC/RZznMhU2BzcHYhX/rWRQvPMCE5k25xs5g9blr2bEU1XItbLS7KY5lfET@XqhCLEvpfgw0WjadhCV0MLeEmkXTR9KvxLKDq2CtRSXNLHYNrtehHq@ylNUrLBKRpGnyJ8l4iLA/RYTWjf6GIMcQhAWYUwVJMFAKzOKnpwjPPP5ILKIisVRC@wcjxAXN6Y3/kxifWkQ8LO@XWQyRWdQJ7tBBxrESRW0bhrqfX4C1KEFDCmw2w1eeQinrjd7iht4/3bHIuEthAVfMFGLPneIxnk0X@x6sve/5wLM/OE@@ufCAXci/52d@rIkHkTdsLlkM2Dm/4voQGnQE74H7lX@iev/hTWdZDZIb4JzDW7PjXw "Haskell – Try It Online")
## Scoring
This is [code-golf](/questions/tagged/code-golf "show questions tagged 'code-golf'") so answers will be scored in bytes with the goal being a smaller score.
## Test cases
### Reject
```
(abs x (var x
uuuuuuuuu
)))(abs x (var x))
app (abs x (var x)) (abs x (var x))
(mmm hummus)
(abs x (var y))
(abs x (abs x (var x)))
(app (abs x (var x)) (var x))
(abs (var k) (var (vark k)))
(abs x (abs y (abs y (var x))))
(abs x(var x))
```
### Accept
```
(abs x (var x))
(abs x (abs y (var x)))
(abs xx (app (var xx) (var xx)))
(app (abs ab (app (var ab) (var ab))) (abs ab (app (var ab) (var ab))))
```
  
[Answer]
# [Perl 5](https://www.perl.org/) `-p`, 86 bytes
Who said this can’t be solved with a regex? ☺
```
$_=reverse=~/^(\)(((\w+) (?=([^)]|(?1))* \4 ))rav|(?1) ((?!(?3))\w+ sb|(?1) pp)a)\()$/
```
[Try it online!](https://tio.run/##hcrBCsIwEIThV1mhhxlFiqjHkAcxVjaQgyB2SSS9iI9uLBa8eptv@C3l27G17uJyqimX5F79gEAAYdpQ4B1OA89P@B25lnAQMmv9WgC/gt@TcyslLqcZlQHs@tagZgKNRTTKgqp5Bn@D/BvwPdrjOt5L29oH "Perl 5 – Try It Online")
Outputs `1` for acceptance or the empty string for rejection. To get around restrictions on lookbehind, I reverse the input and use lookahead instead.
[Answer]
# [Raku (Perl 6)](https://github.com/nxadm/rakudo-pkg) `-p`, 123 bytes
```
my %v;my$r=rx["(abs "(\w+)<!{%v{$0}++}>\s<~~>{--%v{$0}}")"|"(app "<~~>\s<~~>")"|"(var "(\w+)<?{%v{$0}}>")"];$_=so m/^^$r$$/
```
[Try it online!](https://tio.run/##K0gtyjH7/z@3UkG1zDq3UqXItqgiWkkjMalYQUkjplxb00axWrWsWsWgVlu71i6m2Kauzq5aVxciVKukqVQDVFxQoKAEkoBIQwTLEotgJthDTagFScVaq8TbFucr5OrHxakUqajo//8PNgBsZWKSAoQD0p2YpAlnaGoSVKDJ9S@/oCQzP6/4v24BAA "Perl 6 – Try It Online")
First time golfing in Raku (this seemed like an apt challenge to give it a spin), so there's probably room for improvement. It's a simple parse of the text, using the `%v` hash to keep track of existing variables.
[Answer]
## [Tiny Lisp](https://codegolf.stackexchange.com/q/62886/2338), 318
```
(d C(q((E L)(i(e L())0(i(e E(h L))1(C E(t L)))))))(d H(q((le li)(i(e()li)(e le 0)(H(s le 1)(t li))))))(d I(q((L X)(i(e(q abs)(h L))(i(H 3 L)(i(C(h(t L))X)0(I(h(t(t L)))(c(h(t L))X)))0)(i(e(q var)(h L))(i(H 2 L)(i(C(h(t L))X)1 0)0)(i(e(q app)(h L))(i(H 3 L)(i(I(h(t L))X)(I(h(t(t L)))X)0)0)0))))))(d V(q(()(L)(I L()))))
```
This defines a macro `V` (for verify) which can be applied to a list, and will check whether it is of the proper form as defined in the question.
This can't do any checks on a lexical level, as Tiny Lisp has no string input (and not even a string type). Therefore it is running out of competition
Here are some test cases:
```
------examples-from-question-----
((V (abs x (abs y (var x))))  ––→  1)
((V (app (abs x (var x)) (var x)))  ––→  0)
((V (abs x (abs x (var x))))  ––→  0)
----examples-from-TIO----
((V (var x))  ––→  0)
((V (abs vv (var vv)))  ––→  1)
((V (abs xy (var fg)))  ––→  0)
((V (abs x (abs y (var x))))  ––→  1)
((V (app (abs x (var x)) (var x)))  ––→  0)
((V (abs x (app (var x) (var x))))  ––→  1)
((V (app (abs x (app (var x) (var x))) (abs y (app (var y) (var y)))))  ––→  1)
((V (abs x (abs x (var x))))  ––→  0)
((V (abs x (abs y (abs y (var x)))))  ––→  0)
((V (abs (var)))  ––→  0)
---reject---------
((V uuuuuuuuu)  ––→  0)
((V (mmm hummus))  ––→  0)
((V (abs x (var y)))  ––→  0)
((V (abs x (abs x (var x))))  ––→  0)
((V (app (abs x (var x)) (var x)))  ––→  0)
((V (abs (var k) (var (vark k))))  ––→  0)
((V (abs x (abs y (abs y (var x)))))  ––→  0)
((V (abs x (var x)))  ––→  1)
--------accept--------
((V (abs x (var x)))  ––→  1)
((V (abs x (abs y (var x))))  ––→  1)
((V (abs xx (app (var xx) (var xx))))  ––→  1)
((V (app (abs ab (app (var ab) (var ab))) (abs ab (app (var ab) (var ab)))))  ––→  1)
```
The last "reject" case (with the missing space) is accepted, as we are parsing this as a tiny lisp list, not as a lambda.
The test cases with unbalanced parentheses can't even be run.
Here is the code formatted, and with some comments (I've extended the reference implementation of Tiny Lisp to include Python-style line comments).
(The comments all start with `#!` because that can be handled by my automated whitespace-and-comment-remover made for Ceylon.)
```
#! tinylisp.py
#! Parse a lambda for correctness. 
#! Question: https://codegolf.stackexchange.com/q/233453/2338
#! My answer: https://codegolf.stackexchange.com/a/233925/2338
#! checks whether some element is contained in a list.
(d C #! for "contains"
   (q ((E L) #! E = the element to be checked
             #! L = the list in which the element is searched
       (i (e L ())
          0
          (i (e E (h L))
             1
             (C E (t L))
          )
       )
      )
   )
)
#! checks whether a list has a specified length.
#! len = expected length
#! list = list to check
(d H #! for has-length
   (q ((le li) #! le = the asserted length
               #! li = the list to check
       (i (e () li)
          (e le 0)
          (H (s le 1) (t li))
       )
      )
   )
)
#! This is the main working force here.
#! I (for "is-valid") checks (recursively) whether a lambda expression is valid
#! in a given context of defined variable names.
(d I
   (q ((L X)
       #! L = candidate for a lambda function,
       #! X (context) = list of defined variable names
       (i (e (q abs) (h L))
          (i (H 3 L)
             (i (C (h (t L)) X)
                0
                (I (h (t (t L))) (c (h (t L)) X)))
             0)
          (i (e (q var) (h L))
             (i (H 2 L) 
                (i (C (h (t L)) X)
                   1
                   0)
                0
             )
             (i (e (q app) (h L))
                (i (H 3 L)
                   (i (I (h (t L)) X)
                      (I (h (t (t L))) X)
                      0)
                   0)
                0
             )
          )
       )
      )
   )
)
#! V (for "verify") is the entry point to call from the outside.
#! `(V (...))` returns 1 when it's a valid lambda expression, 0 when it is not.
(d V
   (q (()
       (L)
       (I L ())
      )
   )
)
```
[Answer]
# [Curry (PAKCS)](https://www.informatik.uni-kiel.de/%7Epakcs/), 116 bytes
```
p"(var "a x|elem a x=0
p"(app "(a++' ':b)x=a#x+b#x
p"(abs "(a++' ':b)x|all(>'@')a=b#(a:x)
(#)(k++n++")")=p k n
(#[])
```
[Try it online!](https://tio.run/##VU7BCsIwFLv3K0IrrI@ieB5UvHrSu3h43cYYm7V0Tirs3@foTuaQhOSQVFOM333gvhqXJUj94QjJSHMzNE@sxh7FGnMIWNmYAkXpKFlWyTiVcufGv27mYdCn4lwQW6c0l4mEVqR7Y7wxkiTZgB5etFar@4OWJ3ceZYlbbIapbg6XKzSJnFrULwGE2Pk3dmixzTGyOORj@TTTpo5WyEX8AA "Curry (PAKCS) – Try It Online")
`g` returns `0` if there is a match and fails to find a match if there is none.
## Explanation
This looks and sort of works like a Haskell answer might. However Curry's pattern matches are way more powerful than Haskell's because it has a trick up it's sleeve. As well as a functional programming language Curry is a logical language. It has non-determinism.
In Haskell a pattern either matches or it doesn't. In Curry a pattern can match a string multiple ways and it will follow through each to find the one you meant. So
```
p("(app "++a++' ':b++")")
```
Will cold potentially match many things. For example
```
p"(app (var x) (var y))"
```
can break that apart at any space in the string.
Curry will match all of them and attempt to run them. All the bad ones will fail later down the line.
[Answer]
# Scala, 293 bytes
The function that does all the work:
```
def f(s:Any,c:Set[Any]=Set()):Option[Any]=s match{case
s"(var $v)$r"=>Option.when(c(v))(r)case
s"(abs $v $r"=>if(!c(v)&v.matches("[a-z]+"))f(r,c+v).collect{case s")$r"=>r}else None case
s"(app $o"=>f(o,c).collect{case s" $r"=>f(r,c)}.flatten.collect{case s")$r"=>r}case
_=>None}
```
This one simply turns an `Option` into a `Boolean`.
```
f(_)==Some("")
```
[Try it in Scastie!](https://scastie.scala-lang.org/rKZTRkezR8ihidaHyjdUbQ)
Ungolfed:
```
//sexpr is the string to parse, ctx is the context (a Set[String] in reality)
//If valid, it will return a Some containing the rest of the string, otherwise a None
def f(sexpr: Any, ctx: Set[Any] = Set()): Option[Any] = sexpr match {
  case s"(var $varName)$rest" =>
    //Check if varName is defined, and only then return the rest
    Option.when(ctx.contains(varName))(rest)
  case s"(abs $varName $rest" =>
    //Make sure varName isn't already defined and that it's a valid name
    if (!ctx.contains(varName) && varName.matches("[a-z]+"))
      //If so, parse the rest, adding varName to the context
      f(rest, ctx + varName)
        .collect { case s")$rest" => rest } //Ensure there's a matching `)`
    else None //If the name is invalid, so is the expression
  case s"(app $first" =>
    //Try parsing the first argument
    f(first, c)
      //Ensure there's a space after it and parse the rest
      .collect { case s" $rest" => f(rest, ctx) }
      .flatten //Turn the Option[Option[String]] into an Option[String]
      .collect { case s")$rest" => rest } //Ensure there's a matching `)`
  case _ => None //If it's not a var, abs, or app, it's invalid
}
```
]