Solution 1/Proof of solution

This is the proof that Solution 1 fits the constraints of Bitch, Ienai!. It is suggested that you refresh your mind on its' constraints first before reading.

Definitions

• Values are lambdas.
• Transforms are also lambdas.
• Semi-entities are lambdas.
• Properties are the parameters to lambdas, which are themselves also lambdas.
• Definitions are the same thing as properties. In other words, they are also lambdas.
• Entities are also lambdas.
  • Entitydom only occurs in application; using names to refer to semi-entities is only possible within alpha-reduction, which converts parameters (names) into their arguments (semi-entities). Therefore, entities only exist within the context of lambda application.
  • This also makes reference by name the core definition of entities, satisfying the 'entities are always referenced by their definition instead of by value' rule.

The rules

• Properties can be used as semi-entities, and vice versa, because they're both lambdas.
  • The mapping is always unique because all unique lambdas map uniquely to themselves. In other words, X = P(X) for all X.
• Transforms only work on the value of the entity they take in because they're lambdas.
  • Consequently, the PT class doesn't exist (and doesn't actually need to, given the constraints).
  • Transforms also take in one thing before evaluation, since lambdas are automatically curried when they take multiple parameters.
  • : and - don't apply because they're not lambdas, and therefore not transforms.
• Deriving the value from a transform, and vice versa, for the definition of an entity is trivial because they're both lambdas.
  • Entities also always hold the same amount of information as semi-entities, since entitydom relies fully on the information contained within semi-entities.
• U is the universal property.
• The definitions of M, l, and N are derived from the following:
  • The definition of M, written in pseudocode, is M(x: v) → M (read: M takes an entity x of the universal property and returns M). Since all (semi-)entities must have the universal property, this doesn't actually need to be checked; M can just return M directly, hence M = (λ (λ →) → Λ1).
  • The definition of l, in pseudocode, is l(x) → *(y) → [P(x): x] (read: l takes an entity x and returns a transform * that takes an entity y and, if y is P(x), returns x). Since * only needs to return x when y is P(x), it can actually be simplified to *(y) → x, as this also returns x when y is P(x). This simplifies the code to l(x) → *(y) → x, which can be written (λ (λ →) → (λ (λ →) → (λ →))). This is a curried lambda which takes two parameters, which can be written simply as (λ (λ →) (λ → Λ1) → (λ →)).
    • Note that y goes from (λ →) to (λ → Λ1) when un-curried. In the curried lambda, y could share the same definition of (λ →) with x, since the older definition (the one for x) takes precedence (over the one for y); in the un-curried lambda, though, x and y both being (λ →) would collapse them into a single parameter, hence y becomes (λ → Λ1) to avoid that.
  • The definition of N, in pseudocode, is N(x) → *(y) → [P(M): l(x)]. Again, this can be simplified to N(x) → *(y) → l(x), which can be reduced to (λ (λ →) (λ → Λ1) → l (λ →)).