← All problems
Unverified

A Fixed-Point Combinator from B and ω

Let BB and ω\omega be combinators with reduction rules

Bxyz⟶x(yz),ωx⟶xx. Bxyz \longrightarrow x(yz), \qquad \omega x \longrightarrow xx.

An applicative B,ωB,\omega-term is a closed term formed from these two constants using application only. Does there exist such a term YY satisfying

Yx=βηx(Yx) Yx =_{\beta\eta} x(Yx)

for every term xx?

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu