Nghiên cứu này mở rộng Phân biệt Tự động Đồng hình Kết hợp (CHAD) sang các chương trình bao gồm các hàm riêng phần, điều kiện phụ thuộc dữ liệu và các câu lệnh lặp (vòng lặp while). Trong khi vẫn duy trì nguyên tắc ngữ nghĩa bảo toàn cấu trúc của CHAD gốc, chúng tôi giới thiệu 'các phạm trù được lập chỉ mục mở rộng theo vòng lặp' làm cơ sở lý thuyết cho các câu lệnh lặp. Thông qua đó, chúng tôi mở rộng phép biến đổi CHAD với hàm duy nhất bảo toàn cấu trúc (hình thái phạm trù Freyd lặp) ánh xạ khuôn khổ lặp của ngôn ngữ nguồn sang các phạm trù chứa của ngôn ngữ đích và chứng minh tính đúng đắn của phép biến đổi mở rộng bằng mô hình phạm trù. Điều quan trọng là bảo toàn cấu trúc cấu trúc lặp của ngôn ngữ nguồn thông qua việc ánh xạ sang các phạm trù chứa của ngôn ngữ đích.
