Solution 1

Solution 1 is an esolang by User:MarkFan8901 as a solution for Bitch, Ienai!. The proof that Solution 1 is a solution for Bitch, Ienai! can be found here. A variation that doesn't strictly follow its' restraints can be found here.

Introduction

Solution 1 is based off of the lambda calculus. However, instead of using letters to denote parameters, such as λx.x, lambdas use other lambdas, such as λ(λ∅.∅).(λ∅.∅). Both sides of a lambda (called the parameters and body respectively) can be modified, and lambdas are automatically curried to fit their parameters. All the parameters of a given lambda are unique; duplicates are collapsed into their first occurrence. The parameters and body of a lambda are denoted λ_d and λ_b respectively. By default, all lambdas take the universal lambda (written U in the language) and themselves (written Λ) as parameters.

Syntax

The expression λ(λ∅.∅).(λ∅.∅) would be written as (λ (λ →) → (λ →)). Note that here it's valid for lambdas to return nothing (hence the lack of ∅'s), and that (λ →) is a curried lambda with the two default parameters U and Λ (hence the apparent lack of them). Lambdas which contain Λ's use wikipedia:de Brujin indexing to disambiguate which lambda is being referred to; for example, with (λ (λ → Λ1 Λ2) → Λ1), the (Λ1 Λ2) pair refers to the inner and outer lambdas respectively, while the second Λ1 refers to the outer one.

Comments start via ~, and stop at new lines.

Semantics

During execution, alpha-reduction (substituting all occurrences of the parameters in the body with their respective arguments) happens whenever possible (ignoring tautological reductions), with beta-reductions typically happening intermittently between them. Larger expressions take precedence in alpha-reduction over smaller ones. If one lambda is shared across multiple parameters, the oldest one takes precedence. Duplicating a parameter does not change how old it is.

Attempting to remove any default parameters from a lambda will result in an error and will quit execution. The same thing happens when the index for a Λ reaches outside of the outermost lambda.

Program structure

A program consists of a single expression P. P is then implicitly inserted into the following program and ran:

(> U P)
(! (U i i i ...)) ~ infinite number of i's, where i is shorthand for (λ (λ →) → (λ →))

Special forms

Special names

• U is a special name for the universal parameter.
• M is a special name for the lambda (λ (λ →) → Λ1).
• l is a special name for the lambda (λ (λ →) (λ → Λ1) → (λ →)).
• N is a special name for the lambda (λ (λ →) (λ → Λ1) → l (λ →)).

Special procedures

• (: λx λy) adds λx to λy_d.
• (- λx λy) removes λx from λy_d.
• (> λx λy) sets λx_b to λy_b.
• (! λ) outputs the raw dump of λ encoded in Binary lambda calculus.

Note that special procedures are not lambdas (and thus can't be passed through each other), as they have side effects which can't be replicated by lambdas alone. They also destroy their argument(s) when ran.

Miscellaneous

• Λ is special syntax for the identity parameter(s).