لم تزریق برای زبان‌های مستقل از متن
در علوم کامپیوتر، در نظریه زبان‌های فرمال، لم تزریق برای زبان مستقل از متن که از آن با عنوان لم بار-هیلل نیز نام برده می‌شود، روشی است که ویژگی‌های مشترک زبان‌های مستقل از متن را ارائه داده و لم تزریق زبان‌های منظم (رگولار) را تعمیم می‌دهد.
اگر زبان L مستقل از متن باشد، آن‌گاه عدد صحیح P≥۱ موجود می‌باشد (که P طول تزریق می‌باشد) که هر رشته S در L که بلندتر یا مساوی نمادهای P است (برای مثال s|≥p|)، می‌تواند به صورت زیر نوشته شود: S=uvwxy که زیر رشته‌های u, v، w, x و y به این چنین هستند: که مورد ۳ برای همه n≥۰ در L قرار دارد.
لم تزریق زبان‌های مستقل از متن که در ادامه مقاله تنها با عنوان لم تزریق نام برده می‌شود، بیانگر ویژگی مشترک از تمام زبان‌های مستقل از متن است که در واقع ویژگی تمام رشته‌هایی در زبان است که حداقل طول p را دارا هستند و p ثابتی است که طول تزریق نامیده می‌شود و بین انواع زبان‌های مستقل از متن متفاوت است. s را رشته‌ای با حداقل طول p در زبان بنامید. لم تزریق بیان می‌کند که s می‌تواند به ۵ زیر رشته تقسیم شود: s=uvwxy، که در آن vx غیرتهی است و طول vwx حداکثر p می‌باشد؛ بطوری‌که تکرار v و x در s، هر بار رشته‌ای را تولید می‌کند که خودش در زبان وجود دارد (این امکان وجود دارد تا رشته صفر بار تکرار شود که برای حذف v و x از رشته مفید می‌باشد). این فرایند تزریق کپی‌های اضافه v و x، همان چیزی است که از نام لم تزریق برمی‌آید.
زبان‌های متناهی (که منظم و در نتیجه مستقل از متن هستند)، با داشتن p، برابر با حداکثر طول رشته در L بعلاوه یک، بدیهی است که از لم تزریق پیروی کنند و چون رشته‌ای با این طول وجود ندارد، بنابراین لم تزریق نقض نمی‌شود.
لم تزریق گاهی برای اثبات این‌که زبان L داده شده مستقل از متن نیست، به‌کار می‌رود. بدین‌صورت که نشان می‌دهد رشته‌های بلند s دلخواهی در L هستند که بدون تولید رشته‌هایی خارج از L نمی‌توانند تزریق شوند. برای مثال، زبان {L={abc | i> 0، با استفاده از لم تزریق در برهان خلف ثابت می‌شود که مستقل از متن نیست. ابتدا فرض کنید که L مستقل از متن است، با بکارگیری لم تزریق، می‌گوییم عدد صحیح p وجود دارد که طول تزریق زبان L می‌باشد. رشته s=abc را در L در نظر بگیرید. لم تزریق می‌گوید که می‌توانیم s را به صورت s=uvwxy بنویسیم که در آن u, v، w, x و y زیررشته هستند، چنانچه vwx|≤P| و vx| ≥ ۱| و uvwxy برای هر عدد صحیح i ≥ ۰ در L قرار می‌گیرند. با انتخاب s و پیش‌فرض vwx| ≤ p|، به آسانی مشاهده می‌شود که زیر رشته vwx نمی‌تواند بیش از دو نماد (symbol) مجزا داشته باشد؛ بنابراین، یکی از این ۵ احتمال زیر برای vwx وجود دارد.
در هر مورد کاملاً مشهود است که uvwxy برای هر i≠۱ از تعداد برابری از هر حرف برخوردار است؛ بنابراین، uvwxy فرم abc را ندارد و این با تعریف L مغایر است. از این‌رو فرض اولیه مبنی بر این‌که L مستقل از متن است، باید غلط باشد.
علی‌رغم این‌که لم تزریق اغلب برای این به کار می‌رود که اثبات کند زبان داده‌شده مستقل از متن نیست، هیچ‌گونه‌ای توصیفی از زبان‌های مستقل از متن ارائه نمی‌دهد و اگر زبانی شرایط لم تزریق را پوشش ندهد، می‌گوییم مستقل از متن نمی‌باشد.
از طرف دیگر، زبان‌هایی هستند که مستقل از متن نمی‌باشند، اما با این‌حال شرایط لم تزریق را در بر می‌گیرند؛ برای مثال، زبان {L = { bcd | j, k, l ∈ ℕ } ∪ { abcd | i, j ∈ ℕ, i≥۱ برای رشته s=bcd با مثلاً j≥۱، vwx را برای اینکه فقط شامل bها باشد، انتخاب می‌کند و برای رشته s=abcd، vwx را برای اینکه شامل فقط a باشد، انتخاب می‌کند. در هر دو مورد، هر دو رشته تزریق‌شده در L قرار دارند.
اگرچه روش‌های اثبات قوی‌تری مانند لم اوگدن (Ogden)، در دسترس می‌باشند اما حتی آن‌ها هم توصیف دقیقی از زبان‌های مستقل از متن ارائه نمی‌دهند.