Doesn't this program almost surely terminate?

[ccshan]

This program, without commenting out the two lines, is an attempt at flipping coins in search of HTH:

data Flip = H | T;
data Flips = Cons Flip Flips;
data Unit = unit;
define flips = Cons (sample uniform) flips;
define search = \fs: Flips.
  case fs  of | Cons f1 fs1 -> if f1 == T then search fs1 else
  -- case fs1 of | Cons f2 fs2 -> if f2 == H then search (Cons H fs2) else
  -- case fs2 of | Cons f3 fs3 -> if f3 == T then search (Cons T (Cons T fs3)) else
  unit;
search flips

But the compiled FGG gives [0.0]. Commenting out the second line, to search for HT instead, also gives [0.0]. Commenting out both lines, to search for just H, gives [1.0] as desired.

[davidweichiang]

Branch trace adds a -t option to sum_product.py. For ht.txt, it prints:

v=_unit_ [1.0]
v=unit [1.0]
v=H [1.0, 0.0]
v=T [0.0, 1.0]
v=Cons_inst0 _Cons_inst00 _Cons_inst01 [[[1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0]], [[0.0, 1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0]]]
v=_unfoldFlips_inst0_ __unfoldFlips_inst0_0 [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
v=<Unit, Unit, _Unit_>.2 [[0.0], [0.0], [1.0]]
v=<Unit, Unit, _Unit_>.1 [[0.0], [1.0], [0.0]]
v=<Unit, Unit, _Unit_>.0 [[1.0], [0.0], [0.0]]
==_Unit_ [[1.0]]
==Unit & Unit & _Unit_ [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
==_UnfoldFlips_inst0_ [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
==Flip [[1.0, 0.0], [0.0, 1.0]]
v=True [0.0, 1.0]
v=False [1.0, 0.0]
==Unit [[1.0]]
[2]==Flip [[[0.0, 1.0], [1.0, 0.0]], [[1.0, 0.0], [0.0, 1.0]]]
==Flips_inst0 [[1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0]]
sample uniform : Flip [0.5, 0.5]
_this_ [[1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0]]
fs [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
_this_1 [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
_this_0' [[1.0]]
let <_, _this_0', _> = _this_1 in _this_0' [[0.0], [1.0], [0.0]]
case fs of _unfoldFlips_inst0_ _this_1 -> let <_, _this_0', _> = _this_1 in _this_0' [[0.0], [1.0], [0.0]]
search_inst0 [[0.0], [1.0], [0.0]]
fs1 [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
search_inst0 fs1 [[0.0], [1.0], [0.0]]
T [0.0, 1.0]
f1 [[1.0, 0.0], [0.0, 1.0]]
f1 == T [[1.0, 0.0], [0.0, 1.0]]
_this_0 [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
_this_' [[1.0]]
let <_this_', _, _> = _this_0 in _this_' [[1.0], [0.0], [0.0]]
case fs1 of _unfoldFlips_inst0_ _this_0 -> let <_this_', _, _> = _this_0 in _this_' [[1.0], [0.0], [0.0]]
if f1 == T then search_inst0 fs1 else (case fs1 of _unfoldFlips_inst0_ _this_0 -> let <_this_', _, _> = _this_0 in _this_') [[[1.0], [0.0], [0.0]], [[0.0], [1.0], [0.0]]]
case _this_ of Cons_inst0 f1 fs1 -> (if f1 == T then search_inst0 fs1 else (case fs1 of _unfoldFlips_inst0_ _this_0 -> let <_this_', _, _> = _this_0 in _this_')) [[1.0], [0.0], [0.0], [1.0], [0.0], [0.0]]
_unit_ [1.0]
_Cons_inst01 [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
__unfoldFlips_inst0_1 [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
let <_, _, _x0> = __unfoldFlips_inst0_1 in _unit_ [[0.0], [0.0], [1.0]]
case _Cons_inst01 of _unfoldFlips_inst0_ __unfoldFlips_inst0_1 -> let <_, _, _x0> = __unfoldFlips_inst0_1 in _unit_ [[0.0], [0.0], [1.0]]
let _2 : _Unit_ = case _Cons_inst01 of _unfoldFlips_inst0_ __unfoldFlips_inst0_1 -> let <_, _, _x0> = __unfoldFlips_inst0_1 in _unit_ in _unit_ [[0.0], [0.0], [1.0]]
case _this_ of Cons_inst0 _Cons_inst00 _Cons_inst01 -> (let _2 : _Unit_ = case _Cons_inst01 of _unfoldFlips_inst0_ __unfoldFlips_inst0_1 -> let <_, _, _x0> = __unfoldFlips_inst0_1 in _unit_ in _unit_) [[0.0], [0.0], [0.0], [0.0], [1.0], [1.0]]
let _1 : _Unit_ = case _this_ of Cons_inst0 _Cons_inst00 _Cons_inst01 -> (let _2 : _Unit_ = case _Cons_inst01 of _unfoldFlips_inst0_ __unfoldFlips_inst0_1 -> let <_, _, _x0> = __unfoldFlips_inst0_1 in _unit_ in _unit_) in _unit_ [[0.0], [0.0], [0.0], [0.0], [1.0], [1.0]]
H [1.0, 0.0]
fs2 [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
Cons_inst0 H fs2 [[1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0]]
__unfoldFlips_inst0_0 [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
let <_, _, _x> = __unfoldFlips_inst0_0 in _unit_ [[0.0], [0.0], [1.0]]
case fs2 of _unfoldFlips_inst0_ __unfoldFlips_inst0_0 -> let <_, _, _x> = __unfoldFlips_inst0_0 in _unit_ [[0.0], [0.0], [1.0]]
unit [1.0]
let _0 : _Unit_ = case fs2 of _unfoldFlips_inst0_ __unfoldFlips_inst0_0 -> let <_, _, _x> = __unfoldFlips_inst0_0 in _unit_ in unit [[0.0], [0.0], [1.0]]
f2 [[1.0, 0.0], [0.0, 1.0]]
f2 == H [[0.0, 1.0], [1.0, 0.0]]
if f2 == H then search_inst0 (_unapplyFlips_inst0_ (Cons_inst0 H fs2)) else (let _0 : _Unit_ = case fs2 of _unfoldFlips_inst0_ __unfoldFlips_inst0_0 -> let <_, _, _x> = __unfoldFlips_inst0_0 in _unit_ in unit) [[[1.0], [0.0], [0.0]], [[0.0], [0.0], [1.0]]]
_unapplyFlips_inst0_ (Cons_inst0 H fs2) [[1.0, 1.0, 0.0], [0.0, 0.0, 0.0], [0.0, 0.0, 1.0]]
<(case _this_ of Cons_inst0 f2 fs2 -> (if f2 == H then search_inst0 (_unapplyFlips_inst0_ (Cons_inst0 H fs2)) else (let _0 : _Unit_ = case fs2 of _unfoldFlips_inst0_ __unfoldFlips_inst0_0 -> let <_, _, _x> = __unfoldFlips_inst0_0 in _unit_ in unit))), (case _this_ of Cons_inst0 f1 fs1 -> (if f1 == T then search_inst0 fs1 else (case fs1 of _unfoldFlips_inst0_ _this_0 -> let <_this_', _, _> = _this_0 in _this_'))), (let _1 : _Unit_ = case _this_ of Cons_inst0 _Cons_inst00 _Cons_inst01 -> (let _2 : _Unit_ = case _Cons_inst01 of _unfoldFlips_inst0_ __unfoldFlips_inst0_1 -> let <_, _, _x0> = __unfoldFlips_inst0_1 in _unit_ in _unit_) in _unit_)> [[1.0, 1.0, 0.0], [0.0, 0.0, 0.0], [0.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0], [1.0, 0.0, 1.0]]
_unfoldFlips_inst0_ <(case _this_ of Cons_inst0 f2 fs2 -> (if f2 == H then search_inst0 (_unapplyFlips_inst0_ (Cons_inst0 H fs2)) else (let _0 : _Unit_ = case fs2 of _unfoldFlips_inst0_ __unfoldFlips_inst0_0 -> let <_, _, _x> = __unfoldFlips_inst0_0 in _unit_ in unit))), (case _this_ of Cons_inst0 f1 fs1 -> (if f1 == T then search_inst0 fs1 else (case fs1 of _unfoldFlips_inst0_ _this_0 -> let <_this_', _, _> = _this_0 in _this_'))), (let _1 : _Unit_ = case _this_ of Cons_inst0 _Cons_inst00 _Cons_inst01 -> (let _2 : _Unit_ = case _Cons_inst01 of _unfoldFlips_inst0_ __unfoldFlips_inst0_1 -> let <_, _, _x0> = __unfoldFlips_inst0_1 in _unit_ in _unit_) in _unit_)> [[1.0, 1.0, 0.0], [0.0, 0.0, 0.0], [0.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0], [1.0, 0.0, 1.0]]
case _this_ of Cons_inst0 f2 fs2 -> (if f2 == H then search_inst0 (_unapplyFlips_inst0_ (Cons_inst0 H fs2)) else (let _0 : _Unit_ = case fs2 of _unfoldFlips_inst0_ __unfoldFlips_inst0_0 -> let <_, _, _x> = __unfoldFlips_inst0_0 in _unit_ in unit)) [[1.0], [0.0], [0.0], [0.0], [0.0], [1.0]]
_unapplyFlips_inst0_ [[1.0, 1.0, 0.0], [0.0, 0.0, 0.0], [0.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0], [1.0, 0.0, 1.0]]
search_inst0 (_unapplyFlips_inst0_ (Cons_inst0 H fs2)) [[1.0], [0.0], [0.0]]
_unapplyFlips_inst0_ (Cons_inst0 (sample uniform : Flip) flips_inst0) [0.0, 0.0, 0.0]
flips_inst0 [0.0, 0.0, 0.0]
Cons_inst0 (sample uniform : Flip) flips_inst0 [0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
search_inst0 flips_inst0 [0.0]
Cons_inst0 _Cons_inst00 _Cons_inst01 [[[1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0]], [[0.0, 1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0]]]
_unfoldFlips_inst0_ __unfoldFlips_inst0_0 [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0], [0.0, 0.0, 1.0]]
_1 [[1.0]]
_2 [[1.0]]
_x0 [[1.0]]
_Cons_inst00 [[1.0, 0.0], [0.0, 1.0]]
_0 [[1.0]]
_x [[1.0]]
False [1.0, 0.0]
True [0.0, 1.0]

[davidweichiang]

The FGG has an infinite loop:

"flips_inst0" 
-> "_unapplyFlips_inst0_ (Cons_inst0 (sample uniform : Flip) flips_inst0)"
-> "Cons_inst0 (sample uniform : Flip) flips_inst0"
-> "flips_inst0"

[ccshan]

The FGG has an infinite loop:

Ah ok I guess I was too trigger happy with infinite streams...

[davidweichiang]

I see, flips's support is all infinite lists. So there's no bug? But surely printing 0 and pretending nothing is wrong doesn't seem ideal.

[ccshan]

Perhaps what should be more surprising is that the following program defunctionalizes to give the desired nonzero answer. Maybe this is due to the affine-but-not-linear use of the stream fs: Flips.

data Flip = H | T;
data Flips = Cons Flip Flips;
define flips = Cons (sample uniform) flips;
data State = S0 | S1 | S2 | S3;
extern transition: State -> Flip -> State;
data Unit = unit;
extern tick: Unit; 
define search = \s: State. \fs: Flips.
  if s == S3 then unit else
  let _ = tick in
  case fs of Cons f fs -> search (transition s f) fs;
search S0 flips

[davidweichiang]

It would seem that the programs that push back onto the stream are the ones with the problem.

[ccshan]

It would seem that the programs that push back onto the stream are the ones with the problem.

I would instead blame my using a value of recursive type multiple times. Getting the desired answer sometimes can be chalked up to luck. The paper says recursive types are not robust. Should the compiler enforce this?

But surely printing 0 and pretending nothing is wrong doesn't seem ideal.

Maybe I can get an incoming PhD student to work on improving error messages...

[davidweichiang]

Yes, the compiler should enforce nonrobustness. I'm not seeing the nonrobustness -- where is it?

[ccshan]

I'm sorry, I was not clear (even to myself). I'm also sorry I tried and could no longer reproduce the program I believe I wrote in which something like define gen = Cons (sample uniform) gen got reused and managed to generate two different strings. :(

[davidweichiang]

Also, the fact that it worked for H suggests that the problem isn’t the infinite stream per se…

On Thu, May 12, 2022 at 16:33 Chung-chieh Shan @.***> wrote:

The FGG has an infinite loop:

Ah ok I guess I was too trigger happy with infinite streams...

— Reply to this email directly, view it on GitHub https://github.com/diprism/compiler/issues/60#issuecomment-1125397775, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKVY2KYI3RSDKZFZPS3TCDVJVTLBANCNFSM5VZM26DQ . You are receiving this because you commented.Message ID: @.***>