Function lambda_calculus::data::list::pair::zip

source ·
pub fn zip() -> Term
Expand description

Applied to two pair-encoded lists it returns a list of corresponding pairs. If one input list is shorter, excess elements of the longer list are discarded.

ZIP ≡ Z (λzab.IS_NIL b (λx.NIL) (λx.IS_NIL a NIL (CONS (CONS (HEAD b) (HEAD a)) (z (TAIL b) (TAIL a)))) I) ≡ Z (λ λ λ IS_NIL 2 (λ NIL) (λ IS_NIL 2 NIL (CONS (CONS (HEAD 3) (HEAD 2)) (4 (TAIL 3) (TAIL 2)))) I)

Example

use lambda_calculus::data::list::pair::zip;
use lambda_calculus::*;

let list  = || vec![0.into_church(), 1.into_church()].into_pair_list();
let pairs = || vec![(0, 0).into_church(), (1, 1).into_church()].into_pair_list();

assert_eq!(beta(app!(zip(), list(), list()), NOR, 0), pairs());