<!DOCTYPE html>
<html>

  <head>

    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <meta name="description" content="Sci blog jekyll theme">
    <meta name="author" content="AIR RAYA Group">
    <link href='/MyBlog/img/favicon.ico' type='image/icon' rel='shortcut icon'/>

    <title>泽民博客 | Jekyll theme</title>

    <link rel="stylesheet" href="/MyBlog/css/bootstrap.min.css" integrity="sha384-1q8mTJOASx8j1Au+a5WDVnPi2lkFfwwEAa8hDDdjZlpLegxhjVME1fgjWPGmkzs7" crossorigin="anonymous">
    <link rel="stylesheet" href="/MyBlog/css/font-awesome.min.css">
    <link href="/MyBlog/css/simple-sidebar.css" rel="stylesheet">
	<link href="/MyBlog/css/classic-10_7.css" rel="stylesheet" type="text/css">
    <!-- Custom CSS -->
    <link href="/MyBlog/css/style.css" rel="stylesheet">
    <link href="/MyBlog/css/pygments.css" rel="stylesheet">
    <!-- Fonts -->
 <link href="/MyBlog/css/front.css" rel="stylesheet" type="text/css">
 <link href="/MyBlog/css/Josefin_Slab.css" rel="stylesheet" type="text/css">
<link href="/MyBlog/css/Architects_Daughter.css" rel="stylesheet" type="text/css">
<link href="/MyBlog/css/Schoolbell.css" rel="stylesheet" type="text/css">
<link href="/MyBlog/css/Codystar.css" rel="stylesheet" type="text/css">

 <script type="text/javascript" src="/MyBlog/js/jquery-1.12.0.min.js"></script>	

<link href="/MyBlog/css/calendar/common.css" type="text/css"  rel="stylesheet">
<script type="text/javascript" src="/MyBlog/js/calendar/calendar.js"></script>
	<!-- share this -->
	<script type="text/javascript">var switchTo5x=true;</script>
	<script type="text/javascript" src="/MyBlog/js/buttons.js"></script>
	<script type="text/javascript">stLight.options({publisher: "b28464c3-d287-4257-ad18-058346dd35f7", doNotHash: false, doNotCopy: false, hashAddressBar: false});</script>

    <!-- HTML5 Shim and Respond.js IE8 support of HTML5 elements and media queries -->
    <!-- WARNING: Respond.js doesn't work if you view the page via file:// -->
    <!--[if lt IE 9]>
        <script src="/MyBlog/js/html5shiv.js"></script>
        <script src="/MyBlog/js/respond.min.js"></script>
    <![endif]-->
   
   <!--百度统计-->
    <script>
    var _hmt = _hmt || [];
    (function() {
    var hm = document.createElement("script");
    hm.src = "https://hm.baidu.com/hm.js?e965cab8c73512b8b23939e7051d93bd";
    var s = document.getElementsByTagName("script")[0]; 
    s.parentNode.insertBefore(hm, s);
    })();
    </script>
    <script async src="/MyBlog/katex/katex.js"></script>
    <link rel="stylesheet" href="/MyBlog/katex/katex.css">

    <!--轮播图片-->
    <!--script type="text/javascript" src="https://xiazemin.github.io/MyBlog/js/jquery.js"></script>
    <script type="text/javascript" src="https://xiazemin.github.io/MyBlog/js/jquery.stripesrotator.js"></script>
    <script type="text/javascript">
                    $(document).ready(function() {
                    alert($('#rotator_xzm'));
                     alert($('#rotator_xzm').fn);
                    $('#rotator_xzm').stripesRotator({ images: [ "https://xiazemin.github.io/MyBlog/img/BPlusTree.png", "https://xiazemin.github.io/MyBlog/img/linuxMMap.jpeg"] });
                    });
    </script-->

    <!--水印-->
    <script type="text/javascript" src="/MyBlog/js/waterMark.js"></script>
    <script type="text/javascript">
    $(document).ready(function(){
    watermark({watermark_txt0:'泽民博客',watermark_txt1:'zemin',watermark_txt2:(new Date()).Format("yyyy-MM-dd hh:mm:ss.S")});
    })
    </script>
     <!--水印-->
     <!--adscene-->
    <script data-ad-client="ca-pub-6672721494777557" async src="https://pagead2.googlesyndication.com/pagead/js/adsbygoogle.js"></script>

</head>

 <body>
<div id="wrapper">
 <!-- Navigation -->
    <!-- Sidebar -->
        <div id="sidebar-wrapper">
            <ul class="sidebar-nav">
                <li class="sidebar-brand">
                    <a href="/MyBlog">
                        Home
                    </a>
                </li>
                <li>
                    <a href="#">About</a>
                </li>
                <li>
                    <a href="#">Services</a>
                </li>
                <li>
                    <a href="#">Portfolio</a>
                </li>
                <li>
                    <a href="#">Events</a>
                </li>
                <li>
                    <a href="#">Blog</a>
                </li>
                <li>
                    <a href="#">FAQ</a>
                </li>
                <li>
                    <a href="#">Contact</a>
                </li>
            </ul>
        </div>


    <header class="intro-header">
        <div class="container">
            <div class="row">
                <div class="col-lg-12">
                    <div class="heading text-center">
                        <a href="https://xiazemin.github.io/MyBlog/" style="color: #fff; font-size: 4em; font-family: 'Schoolbell', cursive;">泽民博客</a>
                        <a href="#menu-toggle" class="btn btn-default sciblog" id="menu-toggle" style="font-weight: bold;">&#9776; Menu</a>
                    </div>
                </div>
            </div>
        </div>
    </header>

     <script async src="/MyBlog/js/busuanzi.pure.mini.js"></script>

    <script type="text/javascript" src="/MyBlog/js/jquery.js"></script>
    <script type="text/javascript" src="/MyBlog/js/jquery.stripesrotator.js"></script>


 <div class="container">
	<div class="row">
        <div class="box">
                <div class="col-lg-12">
                    <div class="intro-text text-center">
					<h1 class="post-title" itemprop="name headline">lambda 演算中的布尔值和选择</h1>
					<p class="post-meta"> <span itemprop="author" itemscope itemtype="http://schema.org/Person"><span itemprop="name">by 夏泽民</span></span> <time datetime="2018-03-14T00:00:00+08:00" itemprop="datePublished"><i class="fa fa-calendar"></i> Mar 14, 2018</time></p>
					</div>
					 <!-- more --><br />
<p>我们在lambda演算中引入了数字，只差两件事情就可以表达任意计算了：一个是如何表达选择（分支），另一个是如何表示重复。在这篇文章中，我将讨论布尔值和选择，下一篇将介绍重复和递归。</p><br />
<br />
<p>我们希望能够写出形如 if / then / else语句的表达式，就像我们在大多数编程语言做的那样。继像丘奇数那样将数字表示为函数之后，我们也将true和false值表示为对其参数执行一个if-then-else操作的函数：</p><br />
<br />
<p>let TRUE = lambda x y . x <br />
let FALSE = lambda x y . y <br />
于是，现在我们可以写一个“if”函数，它的第一个参数是一个条件表达式，第二个参数是如果条件为真时才进行运算的表达式，第三个参数则如果条件为假时要进行的运算。</p><br />
<br />
<p>let IfThenElse = lambda cond true_expr false_expr . cond true_expr false_expr <br />
此外我们还需要定义常用的逻辑运算：</p><br />
<br />
<p>let BoolAnd = lambda x y . x y FALSE <br />
let BoolOr = lambda x y. x TRUE y <br />
let BoolNot = lambda x . x FALSE TRUE <br />
现在，就让我们过一遍这些定义。让我们先看看BoolAnd：</p><br />
<br />
<p>BoolAnd TRUE FALSE，展开TRUE和FALSE定义：BoolAnd (lambda x y . x) (lambda x y . y)<br />
alpha变换true和false：BoolAnd (lambda xt yt . xt) (lambda xf yf . yf)<br />
现在，展开BoolAnd：(lambda x y. x y FALSE) (lambda xt yt . xt) (lambda xf yf . yf)<br />
beta规约：(lambda xt yt.xt) (lambda xf yf. yf) FALSE<br />
再次beta规约：(lambda xf xf . yf)<br />
于是我们得到结果：BoolAnd TRUE FALSE = FALSE。再让我们来看看BoolAnd FALSE TRUE：</p><br />
<br />
<p>BoolAnd (lambda x y . y) (lambda x y .x)<br />
alpha变换：BoolAnd (lambda xf yf . yf) (lambda xt yt . xt)<br />
展开BoolAnd： (lambda x y .x y FALSE) (lambda xf yf . yf) (lambda xt yt . xt)<br />
beta规约：(lambda xf yf . yf) (lambda xt yt . xt) FALSE<br />
再beta规约：FALSE<br />
所以，BoolAnd FALSE TRUE = FALSE</p><br />
<br />
<p>最后让我们来算算，BoolAnd TRUE TRUE：</p><br />
<br />
<p>展开两个TRUE： BoolAnd (lambda x y . x) (lambda x y . x)<br />
alpha变换： BoolAnd (lambda xa ya . xa) (lambda xb yb . xb)<br />
展开BoolAnd： (lambda x y . x y FALSE) (lambda xa ya . xa) (lambda xb yb . xb)<br />
beta规约： (lambda xa ya . xa) (lambda xb yb . xb) FALSE<br />
beta规约： (lambda xb yb .xb)<br />
所以，BoolAnd TRUE TRUE = TRUE</p><br />

					 <span class='st_sharethis_large' displayText='ShareThis'></span>
						<span class='st_facebook_large' displayText='Facebook'></span>
						<span class='st_twitter_large' displayText='Tweet'></span>
						<span class='st_linkedin_large' displayText='LinkedIn'></span>
						<span class='st_pinterest_large' displayText='Pinterest'></span>
						<span class='st_email_large' displayText='Email'></span>
                </div>
                Category lang
        </div>
	</div>
  
  
       <!--赞-->
    	  <div class="row">
            <div class="col-lg-6">
                <img src="https://xiazemin.github.io/MyBlog/img/webwxgetmsgimg.jpeg"  height="400" width="auto" />
            </div>
          </div>

        <div class="row">
                <div class="col-md-12">
			<div id="disqus_thread"></div>

<div id="gitmentContainer"></div>
<link rel="stylesheet" href="/MyBlog/css/default.css">
<script src="/MyBlog/js/gitment.browser.js"></script>
<script type="text/javascript" src="/MyBlog/js/json2.js"></script>
<script>
var gitment = new Gitment({
    owner: 'xiazemin',
    repo: 'MyBlogComment',
    oauth: {
        client_id: '981ba8c916c262631ea0',
        client_secret: 'a52260ef92de69011ccd1cf355b973ef11d6da0e',
    },
});

var MyGitmentContainer=gitment.render('gitmentContainer');
window.setTimeout(MyGitMentBtnclick,1000); 
//document.ready(function(){ 
//window.onload=function(){}

function MyGitMentBtnclick(){
//var MyGitmentContainer=document.getElementById('gitmentContainer');
	var ele=[],all=MyGitmentContainer.getElementsByTagName("*");
	for(var i=0;i<all.length;i++){
	  if(all[i].className=='gitment-comments-init-btn'){
		MyGitMentBtn=all[i];
		console.log(MyGitMentBtn);
		MyGitMentBtn.click();
	  }
	}
}

</script>



			<!--script>
			/**
			* RECOMMENDED CONFIGURATION VARIABLES: EDIT AND UNCOMMENT THE SECTION BELOW TO INSERT DYNAMIC VALUES FROM YOUR PLATFORM OR CMS.
			* LEARN WHY DEFINING THESE VARIABLES IS IMPORTANT: https://disqus.com/admin/universalcode/#configuration-variables
			*/
			/*
			var disqus_config = function () {
			this.page.url = PAGE_URL; // Replace PAGE_URL with your page's canonical URL variable
			this.page.identifier = PAGE_IDENTIFIER; // Replace PAGE_IDENTIFIER with your page's unique identifier variable
			};
			*/
			(function() { // DON'T EDIT BELOW THIS LINE
			var d = document, s = d.createElement('script');

			s.src = '//airrayagroup.disqus.com/embed.js';

			s.setAttribute('data-timestamp', +new Date());
			(d.head || d.body).appendChild(s);
			})();
			</script>
			<noscript>Please enable JavaScript to view the <a href="https://disqus.com/?ref_noscript" rel="nofollow">comments powered by Disqus.</a></noscript>
			<script id="dsq-count-scr" src="//airrayagroup.disqus.com/count.js" async></script-->
          </div>
       </div>

</div>
<hr>
     <footer>
        <div class="container">
             <a href="/MyBlog/" style="color: green; font-size: 2em; font-family: 'Schoolbell', cursive;">首页</a>
            <div class="row">
                <div class="col-lg-6">
                    <p>Copyright &copy; 2017 465474307@qq.com <p>
                </div>
                <div class="col-lg-6">
                    <p style="float: right;">Jekyll theme by <a href="https://github.com/xiazemin/">夏泽民</a></p>
                </div>
            </div>
        </div>
    </footer>
	
    <!-- jQuery -->
    <script src="/MyBlog/js/jquery-1.12.0.min.js"></script>
    <script src="/MyBlog/js/jquery-migrate-1.2.1.min.js"></script>

    <!-- Latest compiled and minified JavaScript -->
    <script src="/MyBlog/js/bootstrap.min.js" integrity="sha384-0mSbJDEHialfmuBBQP6A4Qrprq5OVfW37PRR3j5ELqxss1yVqOtnepnHVP9aJ7xS" crossorigin="anonymous"></script>
        <!-- Menu Toggle Script -->
    <script>
    $("#menu-toggle").click(function(e) {
        e.preventDefault();
        $("#wrapper").toggleClass("toggled");
    });
    </script>
    <script>window._bd_share_config={"common":{"bdSnsKey":{},"bdText":"","bdMini":"2","bdMiniList":false,"bdPic":"","bdStyle":"0","bdSize":"16"},"slide":{"type":"slide","bdImg":"6","bdPos":"right","bdTop":"100"},"image":{"viewList":["qzone","tsina","tqq","renren","weixin"],"viewText":"分享到：","viewSize":"16"}};with(document)0[(getElementsByTagName('head')[0]||body).appendChild(createElement('script')).src='/MyBlog/shareapi/js/share.js?v=89860593.js?'];</script>


<!-- 2d  -->
<script type="text/javascript" charset="utf-8"  src="/MyBlog/js/L2Dwidget.0.min.js"></script>
<script type="text/javascript" charset="utf-8"  src="/MyBlog/js/L2Dwidget.min.js"></script>
<script type="text/javascript">
 setTimeout(()=> {
/*L2Dwidget.init({"display": {
        "superSample": 2,
        "width": 200,
        "height": 400,
             "position": "right",
                 "hOffset": 0,
        "vOffset": 0
          }
     });
*/
 L2Dwidget
        .on('*', (name) => {
          console.log('%c EVENT ' + '%c -> ' + name, 'background: #222; color: yellow', 'background: #fff; color: #000')
        })
        .init({
          dialog: {
            // 开启对话框
            enable: true,
            script: {
              // 每空闲 10 秒钟，显示一条一言
              'every idle 10s': '$hitokoto$',
              // 当触摸到星星图案
              'hover .star': '星星在天上而你在我心里 (*/ω＼*)',
              // 当触摸到角色身体
              'tap body': '哎呀！别碰我！',
              // 当触摸到角色头部
              'tap face': '人家已经不是小孩子了！'
            }
          }
        });

})
</script>



    <!--html xmlns:wb="http://open.weibo.com/wb">
    <script src="http://tjs.sjs.sinajs.cn/open/api/js/wb.js" type="text/javascript" charset="utf-8"></script>
    <wb:follow-button uid="2165491993" type="red_1" width="67" height="24" ></wb:follow-button-->

      <!--本文来自-->
     <script type="text/javascript">
      /* 仅IE
     document.body.oncopy = function(){
        setTimeout( 
            function () { 
        var text =window.clipboardData.getData("text"); 
        if (text) { 
            text = text + "/r/n本篇文章来源于 xiazemin 的 泽民博客|https://xiazemin.github.io/MyBlog/index.html 原文链接："+location.href; clipboardData.setData("text", text); 
          }
       },
     100 )
    }
     */
     //绑定在了body上，也可以绑定在其他可用元素行，但是不是所有元素都支持copy和past事件。

     /*
$(document.body).bind({
    copy: function(event) {//copy事件
        //var cpTxt = "复制的数据";
        var clipboardData = window.clipboardData; //for IE
        if (!clipboardData) { // for chrome
            clipboardData = event.originalEvent.clipboardData;
        }

        if (event.clipboardData != null/false/undefined) { //ignore the incorrectness of the truncation
        clipboarddata = event.clipboardData;
        } else if (window.clipboardData != null/false/undefined) {
         clipboarddata = window.clipboardData;
        } else { //default to the last option even if it is null/false/undefined
         clipboarddata = event.originalEvent.clipboardData;
        }

        //e.clipboardData.getData('text');//可以获取用户选中复制的数据
        //clipboardData.setData('Text', cpTxt);
        alert(clipboarddata.getData('text'));
        //$('#message').text('Copy Data : ' + cpTxt);
        return false;//否则设不生效
    },paste: function(e) {//paste事件
        var eve = e.originalEvent
        var cp = eve.clipboardData;
        var data = null;
        var clipboardData = window.clipboardData; // IE
        if (!clipboardData) { //chrome
            clipboardData = e.originalEvent.clipboardData
        }
        data = clipboardData.getData('Text');
        //$('#message').html(data);
    }
});     
*/
function addLink() {
    var body_element = document.getElementsByTagName('body')[0];
    var selection;
    selection = window.getSelection();
    var pagelink = "<br /><br />本文来源：xiazemin 的 泽民博客 <a href='"+document.location.href+"'>"+document.location.href+"</a>";
//+document.location.href+当前页面链接
    var copy_text = selection + pagelink;
    console.log(copy_text);
    var new_div = document.createElement('div');
    new_div.style.left='-99999px';
    new_div.style.position='absolute';
    body_element.appendChild(new_div );
    new_div.innerHTML = copy_text ;
    selection.selectAllChildren(new_div );
    window.setTimeout(function() {
        body_element.removeChild(new_div );
    },0);
}
document.oncopy = addLink;
     </script>
    <!--本文来自-->

</div>
  </body>

</html>