Vague question
The most common semantics of the call-by-name $\lambda$-calculus (Hyland/Wadsworth’s observational equivalence $\approx_\text{HNF}$ and Morris’s observational equivalence $\approx_\text{NF}$) are induced by evaluation to head normal forms and to strong normal forms respectively. Since neither the strong reduction nor the head reduction is weak (i.e. both allow to reduce under $\lambda$-abstractions), it is unclear how they relate to semantics of programming languages, whose operational semantics is (nearly) always weak.
This lead to the introduction of Abramsky's lazy $\lambda$-calculus that uses the weak-head reduction, and hence does not evaluate under $\lambda$-abstractions. The observational equivalence $\approx_\text{WHNF}$ of the lazy $\lambda$-calculus is different from the one of the standard $\lambda$-calculus, e.g. distinguishing $\Omega=(\lambda y.yy)(\lambda z.zz)$ from $\lambda x.\Omega$. This leads to a first, rather vague (but refined to a technical question later), question:
How are the non-lazy semantics of the $\lambda$-calculus related to programming languages? (where by programming language I mean any calculus whose operational semantics is defined via a weak reduction)
Motivation
I am looking at unifying the different semantics of the $\lambda$-calculus by embedding it into a polarized calculus (related to Call-by-push-value / the Bang calculus) equipped with a weak head reduction. The lazy call-by-name semantics and call-by-value semantics can be reformulated via a weak-head reduction, which makes the embeddings look very natural. For the non-weak call-by-name semantics, things are more complicated. I have not found a good embedding for $\approx_\text{NF}$ yet, and I'm not sure that one exists.
For $\approx_\text{HNF}$, the embedding works because in the polarized calculus, the semantics only tests convergence of positive terms, which prevents any context from distinguishing $\Omega$ from $\lambda x.\Omega$. In order to make this embedding look more natural, I would like to get a characterization of the semantics that uses a weak reduction in the source, possibly by reifying the "only test convergence on positive terms" part.
Background
The observational equivalence of the $\lambda$-calculus with respect to a pair $X=(\rightsquigarrow, \mathcal{O})$, where $\rightsquigarrow$ is a reduction and $\mathcal{O}$ a set of observables, is defined by $$T\approx_X U \mathrel{\overset{\scriptscriptstyle \text{def}}{=}} \forall K,K[T]\Downarrow_X \text{ iff } K[U]\Downarrow_X $$ (with the quantification on contexts often restricted to contexts that close the terms) where $$\mathord{T\Downarrow_{\rightsquigarrow, \mathcal{O}} }\mathrel{\overset{\scriptscriptstyle \text{def}}{=}}\exists T',T\rightsquigarrow^*T'\text{ and } T'\in\mathcal O$$ The three common observational equivalences are of this shape:
Morris’s observational equivalence is $\approx_{\to,\text{NF}}$ where $\to$ is the strong reduction (i.e. the contextual closure of $(\lambda x.T)U\mapsto T[U/x]$) and $\text{NF}$ is the set of $\to$-normal terms;
Hyland/Wadsworth’s observational equivalence is $\approx_{\to_\text{h},\text{HNF}}$ (or equivalently $\approx_{\to,\text{HNF}}$) where $\to_\text{h}$ is the head reduction and $\text{HNF}$ is the set of head normal forms;
Abramsky's lazy observational equivalence is $\approx_{\to_\text{wh},\text{WHNF}}$ (or equivalently $\approx_{\to,\text{WHNF}}$) where $\to_\text{wh}$ is the weak head reduction, and $\text{WHNF}$ is the set of weak head normal forms.
Technical question and ideal answers
Is there some weak reduction $\rightsquigarrow$ and some natural set of observables $\mathcal{O}$ (possibly in some slight extension of the $\lambda$-calculus), such that Hyland/Wadsworth’s (or Morris’s) observational equivalence is exactly $\approx_{\rightsquigarrow,\mathcal{O}}$?
Changing the range of the quantification on contexts in the definition of $\approx_{\mathcal{O}}$ would also be fine (as long as the new range is reasonable).
A perfect answer would be a story (with a reference to back up all the claims with proofs) that explains why the non-weak semantics of the $\lambda$-calculus are natural even when only considering weak evaluation. Something of this shape: if we extend the $\lambda$-calculus with natural number constants (and a few primitive operations on them), it is natural to think of a term $T$ as representing a partial function $⟦T⟧:\mathbb{N}\rightharpoonup\mathbb{N}$ defined by$$⟦T⟧(n)=\begin{cases}m &\text{if }Tn\to_{\text{wh}}^*m\\\text{undefined}&\text{otherwise} \end{cases}$$ Equality through $⟦-⟧$ under all contexts is (?) exactly $\approx_{\to_\text{wh},\mathbb{N}}$. For some reason (e.g. wanting to keep things minimal, or to extend this to higher-order functions), we remove the natural numbers from the calculus and use their church encoding instead. Because of how the primitive operations on natural numbers are defined, we need to replace the weak head reduction $\to_{\text{wh}}$ by the head reduction $\to_{\text{h}}$ (or the strong reduction $\to$) because otherwise $Tn$ could reduce to e.g. $\lambda x . m x$ and $⟦T⟧(n)$ would be undefined while we want to have $⟦T⟧(n)=m$.
Thoughts
Since defining the semantics via ground terms is standard in the simply typed $\lambda$-calculus, I had hoped to find something about an untyped $\lambda$-calculus with constants that does something similar in an untyped setting in the literature, but could not find it. The only paper I could find that extends the similar way and proves things that look like they could help is "Observability for Pair Pattern Calculi" (where the $\lambda$-calculus is extended with pairs, and a notion that conservatively extends solvability is defined) but it feels like it is too big an extension for my purposes, and I'm not yet sure that it does what I want.
I expect that extending the $\lambda$-calculus by some "positive" constant $c$ (or maybe two) to be necessary and sufficient to get a description of the Hyland/Wadsworth semantics via a weak reduction. Indeed, taking $\mathcal{O}=\{c\}$ looks like it might work: $\approx_{\to,\text{HNF}}$ in the extended calculus should be conservative over $\approx_{\to,\text{HNF}}$ in the $\lambda$-calculus; and in the extended calculus, $\approx_{\to,\text{HNF}}$ should be equivalent to $\approx_{\to_\text{wh},\{c\}}$. If this does work, all the proofs should be routine, but checking everything is still a non-trivial amount of work, so I'd really prefer finding a reference.
