To determine when inversion is possible in the simply typed lambda calculus model, we analyze the types involved and the structure of the pure term ( \alpha ).

Key Observations:

1. Type of ( f ) (σ): If ( f ) has a base type (σ is a base type), inversion is impossible. This is because any closed pure term ( \beta ) of type ( \sigma \to \tau ) (where τ is the type of ( g )) mus...

Short answer

• A uniform, easy-to-check sufficient condition is: α must be part of a definable retraction. That is, there is a pure term β0 with β0 ∘ α ≡βη id. Then for every g and f = M(α) g we can take β = β0 and get g = M(β) f. Your two positive examples are exactly of this kind: one is an isomorphism (argument swap) and the other is a section with a definable left-inverse (a ↦ eval-at-a, left-...

Here is, in essence, what one discovers when one tries to “invert” an equation in a full set‐theoretic model of the simply‐typed λ–calculus:

1. Any pure closed λ–term
   α : τ → σ
   that admits a pure inverse
   β : σ → τ
   must in the model M be a genuine bijection
   M(α) : M(τ) → M(σ).
   Conversely, since M is full (every semantic function is the denotation of ...

This is a fascinating question about the invertibility of lambda calculus equations in full models. Let me analyze this systematically.

The Problem Setup

You're asking when an equation of the form can be "inverted" to find a pure term such that .

Key Observations

1. Type Constraints

The first necessary condition is type compatibility. If $...

First fix some notation.
All terms are closed, purely λ–definable, and are interpreted in a full set–theoretic model M of the simply–typed λ–calculus whose base types are infinite and contain no constants.
For a type σ write Λσ for the closed λ–terms of that type and
M : Λσ → ⟦σ⟧ for their interpretations.

The situation is

 α : σ → τ a closed λ–term
 g ∈ ⟦σ⟧ , f ∈ ⟦τ⟧ such that f = M(α) ...

<think> We are given a full model M of the simply typed lambda calculus with infinite base types. We have two functions f and g in M (not necessarily in the same domain) that are not definable by any pure term. We also have a pure term α such that M(α) g = f. The question is when we can find a pure term β such that g = M(β) f.

First, note that M is a model, so it interprets every pure term. The e...

This is an excellent and subtle question about the nature of definability in the simply typed lambda calculus (STLC). Let's break down the conditions.

Let's denote the function defined by a term t in the model M as F_t, so F_t = M(t). Your starting equation is f = F_α(g). You are asking when there exists a term β such that g = F_β(f).

Substituting f, we get g = F_β(F_α(g)). Thi...

When can you "invert" an equation in the lambda calculus?

This question explores when, given functions f and g in a model M of the simply typed lambda calculus and a pure term α such that M(α)g = f, we can find a pure term β such that g = M(β)f.

Analysis of Examples

Let's analyze the provided examples to understand the pattern:

1. Converse function: When f is the converse of g (f = M(...

Let

 σ , τ be simple types,
 α : σ → τ a closed (pure) λ–term,
 g ∈ M(σ) , f ∈ M(τ) , and
 M(α) g = f.

The question is: when is there a closed λ–term β : τ → σ with

 M(β) f = g ?

In other words, when can one “recover” g from f ?

1 A tautological characterisation
Put

 g ≤ f :⇔ ∃β (closed) . β f = g.

This is the usual notion of relative (or Turing-) definability at higher...