System I Experimentation Tool

To read the details about this system, go here.

Note that you probably need the Mozilla web browser in order to use this experimentation tool.
Other browsers may not offer good enough support for XHTML and JavaScript.

You can also choose from these examples:
If your browser supports JavaScript and DOM, clicking on a term will fill the above box; then you just have to click on the "Experiment with this term" button.
If your browser lacks JavaScript or DOM support, you have to copy an paste the term manually.

• The identity function. No redexes, so the analysis is trivial.
  fn x => x
• Our favorite term.
  (fn x => x x) (fn y => y)
• This term has two apparent beta-redexes after initial reduction to T-normal form. It can be used to check that different strategies of solving the constraints yield the same final result.
  (fn x => a x x) ((fn y => b (c y)) (d e))
• This term has two independent redexes which can commute. It is interesting to see how term reconstruction deals with that.
  (fn y => (fn x => w (x y) z) a) b
• Smallest term for which the strategy of solving the constraint could give different renamings (this implementation always gives the exact same result): (fn x => x (x y)) ((fn z => z) (fn x => a x))
• Rank 6, untypable in predicative System F, typable in impredicative System F
  (fn x => x x) (fn y => y z y)
• Rank 3, untypable in System F_ω
  (fn x => z (x (fn f => fn u => f u)) (x (fn v => fn g => g v))) (fn y => y y y)
• Untypable at any rank
  (fn x => x x) (fn x => x x)
• Rank 3, untypable in F₂ but F₃
  (fn f => fn x => f (f x)) (fn f => fn x => f (f x)) (fn v => fn w => v)
• Rank 4, alternate formulation, untypeable in F₂, but F₃
  (fn two => fn k => two two k)(fn f => fn x => f (f x)) (fn v => fn w => v)
• Rank 5, causes huge blowup. Do not attempt to output skeletons !
  (fn two => fn k => two two two k)(fn f => fn x => f (f x)) (fn v => fn w => v)
• Rank 3
  (fn x => x) (fn y => y y)
• Rank 3
  (fn x => fn y => x) (fn y => y y)
• Rank 1
  (fn x => x) (fn y => y)
• Rank 1
  (fn x => fn y => x y) (fn y => fn x => x y)
• Rank 5
  (fn x => fn y => x y) (fn y => fn x => x y) (fn z => z z)
• Rank 6
  (fn x => x x x) (fn y => y) (fn z => z z)
• Rank 7
  (fn x => x x x x) (fn y => y) (fn z => z z)
• Rank 8
  (fn x => x x x x x) (fn y => y) (fn z => z z)
• Rank 2
  (fn f => fn x => f f x) (fn v => fn w => v)
• Rank 3
  (fn t => fn K => t K) (fn f => fn x => f f x) (fn v => fn w => v)
• Factorial of two, strongly normalizing
  (fn h => h (h (h (fn x => y)))) (fn f => fn n => n (fn v => fn x => fn y => y) (fn x => fn y => x) (fn f => fn x => f x)(fn g => fn x => n (f (n (fn p => fn s => s (p (fn x => fn y => y)) (fn f => fn x => f (p (fn x => fn y => y) f x))) (fn s => s (fn f => fn x => x) (fn f => fn x => x)) (fn x => fn y => x)) g) x)) (fn f => fn x => f (f x))
• Factorial of two, using the Y combinator
  (fn h => (fn x => h (x x)) (fn x => h (x x))) (fn f => fn n => n (fn v => fn x => fn y => y) (fn x => fn y => x) (fn f => fn x => f x)(fn g => fn x => n (f (n (fn p => fn s => s (p (fn x => fn y => y)) (fn f => fn x => f (p (fn x => fn y => y) f x))) (fn s => s (fn f => fn x => x) (fn f => fn x => x)) (fn x => fn y => x)) g) x)) (fn f => fn x => f (f x))
• Factorial of three. Exposed bugs in old implementation. This one works correctly, but the generated files take up to 3.8GB, and it takes about 1 hour on a 2GHz PIII box to get the result. You can see the final judgement here. Yes, the result is the Church numeral for 6.
  (fn h => h (h (h (h (fn x => y))))) (fn f => fn n => n (fn v => fn x => fn y => y) (fn x => fn y => x) (fn f => fn x => f x)(fn g => fn x => n (f (n (fn p => fn s => s (p (fn x => fn y => y)) (fn f => fn x => f (p (fn x => fn y => y) f x))) (fn s => s (fn f => fn x => x) (fn f => fn x => x)) (fn x => fn y => x)) g) x)) (fn f => fn x => f (f (f x)))